Type systems of functional object-oriented languages

12
votes

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 FC for Haskell, which could serve as a "core" for these languages?

1
scalatypespolymorphismocaml
For scala I know there's a formal system underlyng the language, I can't remember if it's vObj. Still I found a useful paper from A.Moors here, but I can't tell its date – pagoda_5b
FYI: The paper was published at FOOL'08 – Malte Schwerhoff
Also see the paper about Scala's dependent object types: lampwww.epfl.ch/~amin/dot/fool.pdf – gzm0

1 Answers

15
votes

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: