It is also more readable (I think) by a human than a tactic-based proof in Coq, say, would be. The proof in Agda is significantly shorter than what the paper proof would be. 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. Overall, this made for a great experience using Agda. It is easy to greet you if we are all named Tom or Tammy. Just remembering the names for everything is a big part of that. Part of what makes theorem proving and dependently typed programming tough is the cognitive burden to keep track of lots of interdependent information. The overloading of constructors is outstanding, for the simple reason that it helps you avoid introducing extra names for similar concepts.That’s exactly what you want in practice, and it’s a pleasure to use. 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. The type refinements in pattern matching (incorporating axiom K, I understand) work simply and naturally.It is just so nice to be able to write something likeįor 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). I had already overcome my foolish bias against these from previous exposure to equational definitions in Haskell.
#SUDO APT GET INSTALL SML NJ CODE#
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. Wrong again! It qualitatively changes the experience to be able to leave those out most of the time. Again, I expected I would not care and would be happy to write out lots of indices to functions explicitly. In most cases, Agda can automatically infer these, and you can omit them where you call the function. For example, to append vectors of length N and M, you need to make N and M extra arguments to the function. With dependent types, you often need lots of specificational data as arguments to functions, just so that later types come out correctly.
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. Using unicode notations in Agda has got me thinking about more general notions of syntax. For all I know, one can define such shortcuts, but the documentation (one of the few negatives) does not seem to say. If I am typing \cdot a lot, maybe I want to type just \. I only wish I could define my own shortcuts for specific symbols. It is just the best, particularly when it comes to formalizing mathematics of whatever kind.
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.
0 kommentar(er)
