小编ser*_*ras的帖子

我开始深入研究依赖类型的编程,并发现Agda和Idris语言最接近Haskell,所以我从那里开始.

我的问题是:它们之间的主要区别是什么？类型系统在两者中是否同样具有表现力？能够进行全面的比较和关于利益的讨论会很棒.

我已经能够发现一些:

• Idris有类型类la Haskell,而Agda有实例参数
• 伊德里斯包括monadic和applicative符号
• 它们似乎都有某种可重新绑定的语法,虽然不确定它们是否相同.

编辑:此问题的Reddit页面中有更多答案:http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

我已经看到GHC的最新版本中支持类型级列表.但是,我需要为应用程序使用类型级别集,并且希望基于类型级别列表实现类型级别集合库.但我不知道从哪里开始:(

在Haskell中是否有任何支持类型级别集的库？