依赖键入的语言最适合“真实世界”。编程吗？

我建议Agda，因为它调用了与Haskell的兼容性。因此，它可能是具有最佳库的依赖类型语言。虽然文档和教程有点乏味，但工具支持也不是很好。说实话，大多数依赖类型的语言目前还没有完全发展。 如果你的需求稍微弱一点，你的语言应该有GADT，那么有两个维护得很好的选项：Scala和Haskell。恕我直言，你可以通过使用GADT获得依赖类型的大部分好处，并且你可以保持类型判断可以启动。 Scala和Haskell都有大量的文档库，工作工具链以及FFI（分别用于Java和C）。两者都有社区使用它们来解决现实问题，如解析和Web开发。     

接受的答案包含错误信息。除非你关闭积极性/终止/宇宙检查，否则Agda中的Typechecking是可判定的。此外，无限进程在Agda中是可编程的，正如IO进程在Haskell中可编程一样：唯一的限制是无限进程在类型检查过程中执行时无法无限展开。你可以在Agda中实现一个图灵机模拟器：你无法说谎它保证终止或说服typechecker以无限制的方式运行它。 但是，我确实认为，在涉及“真实世界”编程时，依赖类型语言仍处于试验阶段。我们还不能支持重型开发，但我们可以在那些关注未来的人中保持一种重要的爱好，而不像过去的功能语言。 正如Twey所建议的那样，伊德里斯是最接近“真实世界”依赖类型语言的候选人。与Agda相比，它更专注于完成工作。我推荐Agda作为更好的工具来掌握依赖类型编程背后的想法，但Idris是更实用的选择。 我很高兴地说，值得考虑最近发布的Haskell作为本次讨论的候选人。从GHC 7.4开始，Haskell开始支持一个有用的类型级数据概念，并且至少使用单例技术（虽然这是一个kludge），我们可以根据运行时值确实有类型（通过使它们依赖于静态变量）约束到相等的运行时间值）。因此，在试验依赖类型的早期阶段，Haskell是一种真正的“现实世界”语言。     

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