1. 34

  2. 49

    I go back and forth between being completely taken with Agda and preferring Idris. I think, in the long run, Agda has enough niceties for me that I will prefer it; but Idris does have some great stuff too.

    Before I jump into a really long list of stuff that I like and dislike about both, it is probably good to say that I really like both languages and I think Idris and Agda are the future of functional programming (ghc keeps moving towards a lot of their ideas even). And they’ve made a bunch of good decisions generally (e.g., both languages use Text instead of String, thank goodness).

    Agda Pros:

    • Total/Complete by-default
    • Arbitrary Unicode identifiers
      • There are only a few reserved characters. Everything else is fair game. This works because Agda requires whitespace between identifiers (2+3 is a valid identifier, so to mean “two plus three”, you use 2 + 3)
      • This is also pervasively taken advantage of in the stdlib (which makes the orthography feel a lot more like a tool itself, à la APL).
    • Arbitrary mixfix
      • The simplest way to explain this is that you can define operators that look like C’s ?: (you can have the operator be in multiple parts); you are not limited to binary operators (as you are in Haskell).
      • Another result of this and of the arbitrary-unicode-identifiers point is that there is functionally no separation between operators and functions in Agda; they work in the same way (which I love).
    • The second-best approach to overloading I’ve ever seen
      • “Do it as much as you want, but you are never allowed to have multiple, incompatible definitions of one identifier in the same scope.” (i.e., every module can export a symbol called map, but you can only have one of them imported at a time if you want to use that same name unqualified)
      • Note that you can either qualify the names accordingly, or you can rename the functions on-import so that there is no ambiguity. You’re call.
      • The best approach, imo, is Haskell’s: “No overloading; use Typeclasses instead.”
    • No Prelude
      • I understand why this bugs a lot of people, but I actually love it. No implicit importing; you only get what you define or import.

    Agda Cons:

    • No Typeclasses! (?)
      • You can emulate them using fancy records (you can even get typeclass-derivation if you’re intense enough about it), but these fancy records are not widely used in the stdlib (last time I checked anyway)
    • Garbage documentation
      • I love a lot of what Agda has done but the wiki and its other docs are tragically out of date
    • Repl that needs a lot of love
      • Barely supported, quite finnicky and a regression from ghci.

    Idris Pros:

    • More closely related to Haskell
      • Where Agda departs significantly from Haskell in how it is written (particularly due to the arbitrary unicode identifiers point above), Idris feels very much like Haskell so it felt simpler to get into.
      • This also means a lot of Idris’s function/operator identifiers are similar/the-same as Haskell’s (this is purely a familiarity argument, but I think it’s worth mentioning)
    • Typeclasses! (?)
    • Much more useful documentation and introduction.
    • Badass REPL
      • For anyone who thinks ghci is good (it is), Idris’s repl is going to feel like you went from a Ford to a Cadilac. It even has fancypants syntax highlighting (on output) built-in!
    • Built-in syntax extensions
      • This is Idris’s way of providing something like arbitrary fixity. You define the function as a regular function, but can then add your own sugar syntax for it. Super cool!
    • Opt-in Laziness
      • Haskell and Agda are both opt-in for strict evaluation. Idris went the other direction which lets you prefer predictability of performance and opt-in to laziness when you need/want it.
    • General Programming is a(n almost?) first-class citizen
      • Where Agda seems rather clearly focused on being a playground for cool, new, dependently-typed things and theorem-proving is the obvious goal of the language, Idris feels a lot more practical for typical usage.

    Idris Cons:

    • Weirdness with inferred types.
      • I’ve brought this up on their bug-tracker before, but the Idris repl does not always infer the most general type. For example: :t 7 returns: 7 : Integer, whereas in ghci, you would get 7 :: Num a => a. This does not affect the language in-practice (you can still use 7 and have it function for Double), but since the language correctly handles those cases, it seems like this is something that should be fixed for consistency.
    • Opt-in Totality
      • I really like that Agda forces you to be total by-default. If you really want to escape its awesome compile-time safety guarantees, you can explicitly jump out of it. I hope more languages move in this direction. Idris allows you to enforce totality, but I wish it were the default.
    • No mixfix or arbitrary-unicode
      • I love that Agda gives you so much freedom with the syntax of the language; Idris’s being closer to Haskell has clear benefits, but these two features are something I have wanted in Haskell for a long time (namely, I really dislike that there is a difference between operators and functions at all, and I love that Agda virtually removed that distinction).

    Okay, that’s most of what I have to say about both languages (sorry for such a giant post, but I like to be thorough).

    Either way, I really like both projects and it’ll be exciting to see how Idris matures as it hits 1.0!

    1. 19

      This is a great post, the sort of thing that keeps lobste.rs in my daily rotation. Thanks.

      1. 9

        All of these things add up and make me prefer Agda to Idris for writing proofs - and not by a little bit. Agda code usually ends up being really nice.

        But Edwin’s research has been in making executables from dependent types. Historically this has been tricky because:

        • Proofs got carried around at runtime
        • Data types such as Nats were represented as linked-lists

        Idris was a pretty important step to being able to actually run verified programs. Agda is not great at being extracted to somewhat efficient code. I think this is by far the greatest thing Idris gives.

        1. 2

          Thanks. Excellent synopsis.