函数式面向对象语言的类型系统

Question

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

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

是否有经过充分研究的正式类型系统，例如 Haskell 的 System F_C，可以作为这些语言的“核心”？

Answer 1

OCaml

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

在核心语言中（不考虑在 模块级别），子类型在 OCaml 中非常受限制，因为子类型 关系不能被抽象出来（没有 有界量化）。语言强调多态 取而代之的是参数化，尤其是“可扩展”类型 支持在其核心使用行多态性（带有便利层 在封闭的此类类型之间进行子类型化）。

有关 OCaml 的类型论表示的介绍，请参阅 Didier Remy 的在线书籍Using, Understanding, and Unraveling the OCaml Language (From Practice to Theory and vice versa) 。它的further reading章节会给你更多的参考，特别是关于面向对象的处理。

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

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

您还应该查看网页A few papers on Caml，它指向一些关于 OCaml 语言的研究文章。

斯卡拉

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

• A Core Calculus for Scala Type Checking，作者 Vincent Cremet、François Garillot、Sergueï Lenglet 和 Martin Odersky，2006 年
• Generics of a Higher Kind，作者：Adriaan Moors、Frank Piessens 和 Martin Odersky，2008 年