键入功能面向对象语言的系统

我想知道现代类型的功能面向对象语言(如Scala和OCaml)如何结合参数多态,子类型和其他功能.

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

是否有一个经过充分研究的正式类型系统,如Haskell的System F _C,它可以作为这些语言的"核心"？

OCaml的

OCaml类型理论的"核心"由系统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的类似页面就是这个页面.与您的问题特别相关的是:

斯卡拉类型检查的核心微积分,由Vincent Cremet,FrançoisGarillot,SergueïLonglet和Martin Odersky,2006年

较高的类泛型,阿德里安摩尔,弗兰克Piessens,马丁Odersky的,2008年