我想知道现代类型的功能面向对象语言（如Scala和OCaml）如何结合参数多态，子类型和其他功能。
他们是基于 系统F.<：或更强或更弱的东西？
是否有一个经过充分研究的正式类型系统，如 系统F.C 对于Haskell来说，它可以作为这些语言的“核心”吗？
我想知道现代类型的功能面向对象语言（如Scala和OCaml）如何结合参数多态，子类型和其他功能。
他们是基于 系统F.<：或更强或更弱的东西？
是否有一个经过充分研究的正式类型系统，如 系统F.C 对于Haskell来说，它可以作为这些语言的“核心”吗？
OCaml类型理论的“核心”包括System F的扩展， 但模块系统对应于F的混合<： （模块可以通过子类型强制转换为更严格的签名）和 Fω。
在核心语言中（不考虑在 模块级别），子类型在OCaml中非常受限制，作为子类型 关系不能被抽象（没有 有限量化）。语言强调多态性 相反，参数化，特别是甚至“可扩展”类型 支持在其核心使用行多态（具有便利层） 封闭的类型之间的子类型）
有关OCaml的类型理论演示的介绍，请参阅Didier Remy的在线书籍， 使用，理解和解开OCaml语言（从实践到理论，反之亦然） 。它的 进一步阅读 本章将为您提供更多参考，特别是关于面向对象的处理。
关于模块系统部分的形式化已经做了很多工作;可以说，ML模块系统没有 自然 适合Fω或F.<：ω 作为核心形式主义（一次，类型参数是 命名 在模块系统中，而不是像lambda-calculi那样按位置传递）。对应的最佳解释之一是 F-ing模块，由Andreas Rossberg，Claudio Russo和Derek Dreyer于2010年首次出版。
Jacques Garrigue还对该语言的更高级功能做了大量工作（不能概括为“只是系统F的语法糖”），即多态变体（等递归结构类型），标记参数和GADT） 。可以找到这些方面的各种描述 在他的网页上，包括多态变体的机械化证明（在Coq中）和宽松值限制。
您还应该查看网页 关于Caml的一些文章，这指向围绕OCaml语言的一些研究文章。
Scala的类似页面是 这个。与您的问题特别相关的是：