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).
2 + 3
7 : Integer
7 :: Num a => a
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!
This is a great post, the sort of thing that keeps lobste.rs in my daily rotation. Thanks.
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:
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.
Thanks. Excellent synopsis.