依赖类型语言最适合"真实世界"编程？

Question

哪些依赖类型的编程语言可用于实际应用程序开发？

这些是我认为重要的一些要点:

• 文件
• 示例程序
• 标准库
• 或至少一个易于使用的外国功能界面
• 一个使用该语言进行现实世界任务的人群
• 工具支持

Answer 1

接受的答案包含错误信息.除非你关闭积极性/终止/宇宙检查,否则Agda中的Typechecking是可判定的.此外,无限进程在Agda中是可编程的,正如IO进程在Haskell中可编程一样:唯一的限制是无限进程在类型检查过程中执行时无法无限展开.你可以在Agda中实现一个图灵机模拟器:你无法说谎它保证终止或说服typechecker以无限制的方式运行它.

但是,我确实认为,在涉及"真实世界"编程时,依赖类型语言仍处于试验阶段.我们还不能支持重型开发,但我们可以在那些关注未来的人中保持一种重要的爱好,而不像过去的功能语言.

正如Twey所建议的那样,伊德里斯是最接近"真实世界"依赖类型语言的候选人.与Agda相比,它更专注于完成工作.我推荐Agda作为更好的工具来掌握依赖类型编程背后的想法,但Idris是更实用的选择.

我很高兴地说,值得考虑最近发布的Haskell作为本次讨论的候选人.从GHC 7.4开始,Haskell开始支持一个有用的类型级数据概念,并且至少使用单例技术(虽然这是一个kludge),我们可以根据运行时值确实有类型(通过使它们依赖于静态变量)约束到相等的运行时间值).因此,在试验依赖类型的早期阶段,Haskell是一种真正的"现实世界"语言.

Answer 2

我建议Agda,因为它调用了与Haskell的兼容性.因此,它可能是具有最佳库的依赖类型语言.虽然文档和教程有点乏味,但工具支持也不是很好.说实话,大多数依赖类型的语言目前还没有完全发展.

如果你的需求稍微弱一点,你的语言应该有GADT,那么有两个维护得很好的选项:Scala和Haskell.恕我直言,你可以通过使用GADT获得依赖类型的大部分好处,并且你可以保持类型判断可以启动.

Scala和Haskell都有大量的文档库,工作工具链以及FFI(分别用于Java和C).两者都有社区使用它们来解决现实问题,如解析和Web 开发.

Answer 3

Agda并非旨在成为通用编程语言.ATS是一种依赖类型的语言,专为低级编程而设计,虽然它不如Agda优雅.Idris是一种依赖类型的语言,专为高性能应用程序级别的程序而设计.