This summer, a bunch of us here at U. Iowa were learning Agda, and I thought I’d write up some of my thoughts on the system, now that we have used it a little.  Overall, I found it to be a great tool, with numerous very nice design ideas.  The positives:

• The latex-style syntax for unicode, which I gather is supported in some other tools like Isabelle, is fantastic.  One can type \forall and get ∀.  I thought I would not care much and not use it, and was surprised to find how much I like having these notations available in code.  It is just the best, particularly when it comes to formalizing mathematics of whatever kind.  I only wish I could define my own shortcuts for specific symbols.  If I am typing \cdot a lot, maybe I want to type just \. or something.  For all I know, one can define such shortcuts, but the documentation (one of the few negatives) does not seem to say.  Using unicode notations in Agda has got me thinking about more general notions of syntax.  For example, what about 2-dimensional syntax, where I can supply any scalar vector graphics image as the definition of a symbol?  Then I could design my own notations, and have inputs and outputs coming in and out of different ports on a square displaying that image.
• The support for implicit arguments to functions is very good.  With dependent types, you often need lots of specificational data as arguments to functions, just so that later types come out correctly.  For example, to append vectors of length N and M, you need to make N and M extra arguments to the function.  In most cases, Agda can automatically infer these, and you can omit them where you call the function.  Again, I expected I would not care and would be happy to write out lots of indices to functions explicitly.  Wrong again!  It qualitatively changes the experience to be able to leave those out most of the time.  Code becomes much, much shorter, and when you get lucky and everything lines up correctly, and Agda can figure out instantiations, then it is quicker to write, with less cognitive burden.  This is really a great feature.
• Equational definitions are fantastic.  I had already overcome my foolish bias against these from previous exposure to equational definitions in Haskell.  It is just so nice to be able to write something like

 [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys) 

for append, rather than first abstracting the arguments and then doing the pattern matching and recursion, as one would in OCaml (which is still my go-to programming language, despite all this coolness in these other languages).

• The type refinements in pattern matching (incorporating axiom K, I understand) work simply and naturally.  You match on something of type a ≡ b, you cover that case with just refl, and the type checker knows a must be definitionally equal to b.  That’s exactly what you want in practice, and it’s a pleasure to use.
• The overloading of constructors is outstanding, for the simple reason that it helps you avoid introducing extra names for similar concepts.  Part of what makes theorem proving and dependently typed programming tough is the cognitive burden to keep track of lots of interdependent information.  Just remembering the names for everything is a big part of that.  Fewer names, less cognitive load.  It is easy to greet you if we are all named Tom or Tammy.

Overall, this made for a great experience using Agda.  For example, I formalized Kripke semantics for intuitionistic propositional logic (actually, bi-intuitionistic logic, but that is another post), and proved monotonicity of the semantics, a standard property.  The proof in Agda is significantly shorter than what the paper proof would be.  It is also more readable (I think) by a human than a tactic-based proof in Coq, say, would be.  This is really the first time I felt as thought some result was easier to prove in a theorem prover than slogging it out in LaTex.  I am not saying Agda is unique in enabling this, but it is interesting to me that the first time I have had this feeling (having formalized a number of other things in Coq and other provers, including a couple of my own) is in Agda.

Ok,  now quickly for some constructive criticism:

• The documentation needs to be improved.  I know it is a nuisance to document things, and it seems, from the Agda wiki,  that maybe the documentation has been getting updated or migrated or something.  But it’s not too great right now.  There are many little sources to consult (this tutorial for how to use the Agda emacs mode, these lecture notes for how this or that feature of the language works, this old reference manual for this, a new reference manual for that).  It is irritating.  Agda needs a single consolidated reference manual with all features covered with examples.
• The standard library needs better documentation, too.  Mostly the intended use model seems to be to browse the standard library.  This is not too fun.  The organization of the standard library has some annoyances, like central definitions put in Core.agda files in subdirectories, rather than in the expected file.  Either some kind of agdadoc tool that could generate just type signatures and comments in HTML from the library code, or else a real reference manual for the standard library, would improve usability a lot.  Just look at OCaml’s standard library documentation for a very nice example.
• Error messages involving meta-variables and implicit variables can be hard to decode.  Giving good error feedback with type inference is known to be a tough problem, and it is exacerbated with the dependently typed setting.  I think we need more research (or if it’s already been done, more implemented research) on how to let the programmer interact with a type checker to explore the state the type checker has gotten into when it found a type error.  Mostly Agda’s error messages are reasonable, but once higher-order meta-variables and implicit arguments get involved, it can be pretty confusing to figure out why it’s having trouble typing my term.
• Compilation is a bit funny right now.  Compiling hello-world in Agda took a couple minutes, and generated a 10 megabyte executable.  Wow!  It’s because it is first compiling a big chunk of the standard library to Haskell, and then calling the Haskell compiler.  It still seems too slow, and generating too big an executable.  I asked one major Agda user this summer about this, and he said he had never tried to compile a program before!  So many people are just running the type checker, and using Agda as a theorem prover.  But it does compile, and it can do rudimentary IO with Haskell’s IO monad (this is a plus I did not list above).

Ok, so that’s my feedback from learning Agda this summer.  I’d love to hear others’ experiences or thoughts in the comments!

1. I don’t use the standard library; I have my own. Actually, one for HoTT and one older one from pre-HoTT days. Not sure how this influences executable size. I agree that the standard library is hard to get your head around sometimes—it’s written in a very abstract/parametrized style.

You can make your own abbreviations for unicode by adding some hooks to quail; for example, I have this in my .emacs:

‘(mapc (lambda (pair)
(quail-defrule (car pair) (cadr pair) “TeX”))
‘((“\\comp” “∘”)
(“\\ep” “⁺”)
(“\\en” “⁻”)
(“\\pp” “≃”)
(“\\lp” “λ≃”)
(“\\one” “¹”)
(“\\two” “²”)
(“\\three” “³”)
(“\\s1” [“S¹”])
(“\\s2” [“S²”])
(“\\s3” [“S³”])
(“\\es” [“≃〈 〉”])
(“\\command” “⌘”)
(“\$[” “⟦”) (“\$]” “⟧”)
; If you find it awkward to write comments using the TeX input
; method the following bindings may make life more bearable
; for you:
(“–” [“–“])
(“—” [“—“])
; Add more keybindings here.
)))

2. Thanks a lot for the tip on the syntax definitions, Dan!