1. 15
  1. 3

    What a coincidence, I was looking into learning Agda yesterday. Considering this short guide is far from complete and its last chapter is marked deprecated, are there any other good resources for learning Agda? As far as the ideas themselves of dependent types go, I’ve read “The Little Typer”, which gave me a good understanding of the fundamentals, but I’d like to read some more about things specific to Agda and the ways it is unique in the proof assistant landscape.

    1. 3

      I do wish there was a detailed comparison review / table / something of tools in the dependent types / proof assistant space… As someone trying to learn about this area, I currently find it quite hard to work how to choose between Coq, Idris, Agda, Lean, etc. At the moment, it feels like the people who know the area deeply enough to write such a thing are also heavily involved in one specific camp…

      If anyone knows of such a resource, please do share it!

      1. 5

        I don’t know of such a resource, but as a very quick overview:

        • Coq really is a theorem proved based on tactics, and supporting proof automation. Its syntax is ML-like. In Coq, one can write automated procedures to get rid of similar (or not-so-similar) cases for you. A great example is the Lia tactic, which automatically solves many proof goals with equalities and inequalities in them using some kind of algorithm. You never have to see the final proof object. It’s quite convenient. Another thing Coq has is extraction. It has built-in functionality for turning Coq code into, say, Haskell or OCaml. It’s not ideal, but you can verify a Coq program and then use it in some other project. The main downside of the language is, to me, its size. There are multiple sub-languages in Coq, with similar but different syntaxes. It’s a lot to learn. I also think the documentation could use some work.
        • Where Coq lets you prove things via “tactics”, Agda lets you do so using standard proof objects and functions. I’ve seen it used for formalized mathematics and computer science (“Programming language foundations in Agda”, “Univalent foundations in Agda”), and also in multiple recent PL papers (a not-so-recent example is Hazel, a programming language whose semantics were formalized in Agda I believe). However, it’s also a much nicer language for actual dependently typed programming. It’s got a Haskell-like syntax and also some pretty nice support for custom notation and operators.
        • Idris is also a Haskell-like language and it’s really geared towards dependently typed programming rather than proofs. It has some helper functions in its standard library for basic things (replacing one value with another equal value in a type, for example) but it’s far from convenient to write. In fact, Idris2 is (last I checked) not even sound. In it, Type : Type, which I believe can lead to a version of Russel’s paradox. Thus, you can technically prove anything. Idris’s new tagline is “language for type-driven development”. The approach that Edwin, the language’s creator, wants you to take is that of writing down types with a hole, and then gradually filling in the hole with code using the types to guide you.

        I know you asked for a detailed review, but I thought maybe this would help.

        1. 1

          Thank you! Does anyone know enough about Lean to add a quick overview of it?

      2. 3

        Are there any other good resources for learning Agda

        I’m going through PLFA, and there is an ongoing Discord study group here. For a concise 40-page introduction to Agda, see Dependently Typed Programming in Agda.

        You might find some of the links I collect here on Agda interesting: https://www.srid.ca/agda

        1. 2

          Programming Language Foundations in Agda looks useful. Haven’t had the chance to dig into it yet though.

          1. 1

            If you’re interested in using Agda as a vehicle to learning type theory, there’s also Introduction to Univalent Foundations of Mathematics with Agda, which isn’t exactly beginner material, though. Agda also itself supports cubical types, which kind of incepts the whole thing.

            In general, most of the material in Agda I’ve seen is oriented towards type theory and/or programming language research. It’d be interesting to see other mathematics as well.

            1. 1

              Thanks for the pointer! How feasible would it be in your opinion to understand this with only a few definitions’ worth of category theory knowledge?