12

我想知道现代类型化的函数式面向对象语言（如 Scala 和 OCaml）究竟是如何结合参数多态性、子类型化和其他特性的。

它们是基于System F <:，还是更强或更弱的东西？

是否有一个经过充分研究的形式类型系统，比如用于 Haskell 的System F C，它可以作为这些语言的“核心”？

4

1 回答 1

15

OCaml

OCaml 类型理论的“核心”由系统 F 的扩展组成，但模块系统对应于 F <:（ 模块可以通过子类型强制转换为更严格的签名）和 Fω 的混合。

在核心语言中（不考虑模块级别的子类型化），子类型化在 OCaml 中受到非常严格的限制，因为子类型化关系不能被抽象化（没有有界量化）。该语言强调多态参数，特别是它支持的“可扩展”类型在其核心使用行多态（在封闭的此类类型之间有一个便利的子类型层）。

有关 OCaml 的类型理论演示的介绍，请参阅 Didier Remy 的在线书籍，使用、理解和解开 OCaml 语言（从实践到理论，反之亦然）。它的进一步阅读章节会给你更多的参考，特别是关于面向对象的处理。

在模块系统部分的形式化方面已经做了很多工作；可以说，ML 模块系统并不自然地适合 Fω 或 F <: ω作为核心形式（有一次，类型参数在模块系统中命名，而不是像 lambda-calculi 中那样按位置传递）。对通信的最佳解释之一是F-ing modules，由 Andreas Rossberg、Claudio Russo 和 Derek Dreyer 于 2010 年首次出版。

Jacques Garrigue 还在语言的更高级特性（不能概括为“只是系统 F 上的语法糖”）上做了大量工作，即多态​​变体（等递归结构类型）、标记参数和 GADT） . 这些方面的各种描述可以在他的网页上找到，包括多态变体的机械化证明（在 Coq 中）和放宽的值限制。

您还应该查看网页Asome paper on Caml，其中指向一些围绕 OCaml 语言的研究文章。

斯卡拉

Scala 的类似页面是这个。与您的问题特别相关的是：

于 2013-05-24T11:41:20.353 回答