最适合“现实世界”编程的依赖类型语言？ [关闭]答案

【问题标题】：Dependently typed language best suited to "real world" programming? [closed]最适合“现实世界”编程的依赖类型语言？ [关闭]
【发布时间】：2011-06-05 18:42:33
【问题描述】：

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

以下是我认为很重要的几点：

文档
示例程序
标准库
或者至少是一个易于使用的外部函数接口
一个使用该语言完成现实世界任务的社区
工具支持

【问题讨论】：

可能更适合programmers.stackexchange.com...
任何一个都可以使用。您需要为您的问题提供更多背景信息。
图灵完备性怎么样？这也有要求吗？另外，当您说“现实世界的任务”时，您的意思是“开发应用程序”而不是“证明定理”，对吧？
@jzd：我应该提供什么样的“上下文”？
@sepp2k：我的问题包含“应用程序开发”一词。 ;)

标签： programming-languages dependent-type

【解决方案1】：

接受的答案包含错误信息。 Agda 中的类型检查是可确定的，除非您关闭积极性/终止/宇宙检查。此外，无限进程在 Agda 中是可编程的，就像 IO 进程在 Haskell 中是可编程的一样：唯一的限制是无限进程在执行时不能无限展开在类型检查过程中。你可以在 Agda 中实现一个图灵机模拟器：你不能说谎保证它会终止或说服类型检查器以无限制的方式运行它。

不过，我同意依赖类型语言在“现实世界”编程方面仍处于试验阶段。我们还不能支持繁重的开发，但我们可以在那些着眼于未来的人中维持一个重要的爱好，就像过去的函数式语言一样。

正如 Twey 所建议的，Idris 是最接近“现实世界”依赖类型语言的候选者。它比 Agda 更专注于完成工作。我推荐 Agda 作为更好地掌握依赖类型编程背后的思想的工具，但 Idris 是更实用的选择。

我很高兴地说，值得考虑将 Haskell 的最新版本作为本次讨论的候选者。从 GHC 7.4 开始，Haskell 开始支持一个有用的类型级别数据概念，并且至少使用 singleton 技术（虽然这是一个杂项），我们真的可以根据运行时值来拥有类型（通过使它们依赖于限制为相等的运行时值的静态变量）。因此，Haskell 在试验依赖类型的早期阶段是一种真正的“真实世界”语言。

【讨论】：

感谢您的回答。 Haskell 的能力有多远？听起来在这方面可以和 Scala 媲美。
我不太了解 Scala，无法进行比较。然而，Haskell 正在以相当快的速度朝着依赖类型的方向发展。种类多态性（如在 GHC 7.6 中）使得可以有效地处理通过自动将类型提升到种类级别而创建的所有新种类。我的赌注是 Haskell 在这方面领先于 Scala，但我很高兴被证明是错误的。
呃，嗯，让我补充一下，我的 ICFP2012 谈话 youtube.com/watch?v=XGyJ519RY6Y 中的开发 t.co/fB8sFizL 是一种逐渐变得更加依赖类型的练习。 Haskell 可以轻松进入第 4 部分，但第 5 部分的希望太大了。另请参阅 stackoverflow.com/questions/10656402/… 了解可能的示例。

【解决方案2】：

Agda 并非设计为通用编程语言。 ATS 是一种依赖类型语言，专为低级编程而设计，尽管它不如 Agda 优雅。 Idris 是一种新兴的依赖类型语言，专为高性能应用程序级程序而设计。

【讨论】：

【解决方案3】：

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

如果您的语言应该有GADT's 的要求稍弱，那么有两个维护得很好的选项：Scala 和 Haskell。恕我直言，您通过使用 GADT 获得了依赖类型的大部分好处，并且您保持类型检查可决定启动。

Scala 和 Haskell 都有大型且文档齐全的库、一个工作工具链以及 FFI（分别针对 Java 和 C）。两者都有社区使用它们来解决现实世界的问题，例如 parsing 和 web development.

【讨论】：

我使用 scala 已经有一段时间了，但我没有使用过 GADT。它们与依赖类型有何关系？
GADT 是依赖类型和常规参数类型之间的有用中间步骤。与大多数类型系统相比，您的类型更加强大，并且没有像依赖类型那样具有完整（不可确定）的类型系统。拥有不可确定的类型系统有点问题，因为类型检查有很小的机会无限循环。因此，除非您知道您将需要依赖类型的额外类型信息，否则您最好停止使用 GADT。因为它们允许你做比大多数类型系统更酷的事情，同时仍然是可判定的。
作为参考，OCaml 现在也支持 GADT。