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

Question

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

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

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

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 演算中那样按位置传递)。该信件的最佳解释之一是 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 年