我想知道现代类型化的功能化面向对象的语言(例如Scala和OCaml)如何将参数多态性，子类型化及其其他功能结合在一起。
它们是基于System F还是更强或更弱的东西？
是否有经过充分研究的正式类型系统，例如Haskell的System F，可以用作这些语言的“核心”？
最佳答案
OCaml
OCaml类型理论的“核心”包括系统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 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。与您的问题特别相关的是: