Type systems of functional object-oriented languages

Question

I would like to know how exactly modern typed functional object-oriented languages, such as Scala and OCaml, combine parametric polymorphism, subtyping and other their features.

Are they based on System F_<:, or something stronger, or weaker?

Is there a well-studied formal type system, like System F_C for Haskell, which could serve as a "core" for these languages?

Answer 1

OCaml

The "core" of OCaml type theory consists of extensions of System F, but the module system corresponds to a mix of F_<: (modules can be coerced into stricter signature by subtyping) and Fω.

In the core language (without considering subtyping at the module level), subtyping is very restricted in OCaml, as subtyping relations cannot be abstracted over (there is no bounded quantification). The language emphasizes polymorphic parametrism instead, and in particular even the "extensible" type it supports use row polymorphism at their core (with a convenience layer of subtyping between closed such types).

For an introduction to type-theoretic presentations of OCaml, see the online book by Didier Remy, Using, Understanding, and Unraveling the OCaml Language (From Practice to Theory and vice versa) . Its further reading chapter will give you more reference, in particular about the treatment of object-orientation.

There has been a lot of work on formalizations of the module system part; arguably, the ML module systems do not naturally fit Fω or F_<:^ω as a core formalism (for once, type parameters are named in a module system, instead of being passed by position as in lambda-calculi). One of the best explanations of the correspondence is F-ing modules, first published in 2010 by Andreas Rossberg, Claudio Russo and Derek Dreyer.

Jacques Garrigue has also done a lot of work on the more advanced features of the language (that cannot be summarized as "just syntactic sugar over system F"), namely Polymorphic Variants (equi-recursives structural types), labelled arguments, and GADTs). Various descriptions of these aspects can be found on his webpage, including mechanized proofs (in Coq) of polymorphic variants and the relaxed value restriction.

You should also look at the webpage A few papers on Caml, which points to some of the research article around the OCaml language.

Scala

The similar page for Scala is this one. Particularly relevant to your question are:

• A Core Calculus for Scala Type Checking, by Vincent Cremet, François Garillot, Sergueï Lenglet and Martin Odersky, 2006
• Generics of a Higher Kind, by Adriaan Moors, Frank Piessens, and Martin Odersky, 2008