functional-programming - Gallina 和 OCaml 是什么关系？

Question

我了解到 Coq 是用 OCaml 编写的，但它的规范语言是 Gallina。除了它们都是函数式编程语言之外，这两种语言有什么关系？

Answer 1

这是一个有点负荷的问题。

Gallina 可以独立于 OCaml 存在，但是，作为 lambda 演算，它与它共享一些构造和语义，并且在 OCaml 世界中开发，它也共享一些具体的语法。但是 OCaml 不适合代替 Gallina。

一些相似之处：

• 它们共享受 lambda 演算启发的函数式语言。
• 它们具有相似的代数数据类型声明（尽管在允许和可表达方面存在很多差异）。

一些（主要）差异：

• Gallina 有依赖类型，而 OCaml 有一个类型系统，它接近带有一些子类型的 prenex 多态系统 F……我不知道如何称呼它，但它在某些方面不如依赖类型具有表现力，虽然它有一些加利纳没有的额外功能。
• Gallina 是完全的，这意味着所有函数都必须在语法上表现良好，要么明确终止，要么明确进行计算。OCaml 是一种更通用的语言，其中不终止是可以的。
• Gallina 是纯粹的，而 OCaml 具有副作用的原语。
• 如果您愿意，Gallina 是“仅功能性的”。OCaml 有一个对象的概念，一些看起来“势在必行”的特征（由于前面列出的所有差异）。

事实上，从历史上看，ML（OCaml 是其中的一些变体）对于 LCF 之于 LCF 之于 Gallina！:-D（哦，天哪，我可能会因为这张纸条而受到一些愤怒的评论......）