3 ms·

Any thoughts on Agda? I've always thought that since it's embedded in Haskell, even though it's less 'practical' than Idris it would benefit from the extensive

Any thoughts on Agda? I've always thought that since it's embedded in Haskell, even though it's less 'practical' than Idris it would benefit from the extensive libraries that Haskell brings to the table.

Zalastax 8y ago
Usually, Agda programs would not use Haskell libraries very much, even though they could. The reason seems to be that it is an unstable language and we are still figuring out how to do dependent types correctly. To me, working in Agda is like working in a very powerful version of Haskell, but for most people it's more about working in a research language. Idris and Agda are quite similar: don't build a company on them, but expect really cool ideas to spawn from them. Dependent types is really an awesome idea.