Hacker News Reader

For enlightenment learn Agda. For transcendence, learn Idris ;) I would like to learn either Idris or Agda for their relationship to mathematics, but I am tempted by Idris also being able to do general programming with its compile targets. How does Agda compare to Idris on this point?

View on HN

Runtime performance for Agda... well, it leaves a lot to be desired, at least with respect to the MAlonzo compiler. For example, operations on the natural numbers à la Data.Nat get very slow very quickly-- but while the representation used by Data.Bin speeds things up a lot, you just can't do the same Peano-style structural induction on it.

My understanding is that Agda puts much less emphasis on general programming. It's more focused on proving.

Reply on news.ycombinator.com