3 ms·
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 tempt
by eggy 12y ago
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?
- pseudonom- 12y agoMy understanding is that Agda puts much less emphasis on general programming. It's more focused on proving.
- sjolsen 12y agoRuntime 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.