A long story about MLF, part 1: Introduction, ML
This blog post and its hopefully forthcoming siblings are adapted from a "rapport de M1" (master thesis) describing an internship last year (spring and summer). I’m not used to writing in english, and this document was written in a very short time span, so it’s far from perfect. I’m willing to refine and maintain it (in particular as other people may have to maintain and evolve the associated software I produced during my internship), so please do not hesistate to spot mistakes and/or ask for clarifications.
I will not publish here the full document in one fatal blow. I plan to progressively send chunks of it, so that the people on the receiving end have the time to read it, and, hopefully, engage discussion.
My aims in using this unusual medium/content interaction (a student report on a programming blog ?) is primarily to inform people I know about what I’ve worked on, and perhaps give them the opportunity to learn a little more about ML, System F, type systems and type inference.
I’ve tried to keep it accessible to non-specialists, and will probably skip the second and third part of my report, which are much more technical. Of course, those were the parts about what I’ve personally tried to do during my internship; the first part (the most interesting) is about serious research by other people.
This thesis presents the context and nature of the work during a six-month internship at Gallium, a research team of the Institut National de Recherche en Informatique et en Automatique (INRIA) which is specialized in the design, formalization and implementation of programming languages and systems.
My advisor was Didier Rémy, a senior member of the team, which specializes, among other things, in type systems and type inference. The internship subject was MLF, a type system developped by Didier and two of his former PhD students, Didier Le Botlan and Boris Yakobowksi.
MLF is a rich research topic which, despite interest and research by other people and teams outside Gallium, has not yet been integrated in the "mainstream" common knowledge of our discipline. A significant part of the intership time was dedicated to the study of the subject bibliography, and of the type system itself: despite very attractive properties, it is a complex system that has not yet been presented in a way making possible to thouroughly understand it in a calm afternoon of scholarly readings.
The main part of this document will be dedicated to an informal presentation of the MLF system. I’m not trying to be formal and exhaustive (nor could I, given size limits), only to convey the necessary intuition to understand the specific problematics of my internship subject. The reader interested in a more complete description of the different part of MLF will be redirected to the growing existing litterature.
The other parts of my internship dedicated to my work — Gallium team is rich in distractions; I won’t describe here the quite enjoyable pauses café(s), the very interesting research seminar, etc. — was dedicated to research and implementation.
The research part was dedicated to an extension of MLF with explicit polymorphism and higher-order types, which we could name MLFω. This had already been the subject of an internship by Paolo Herm’s last year, and we hoped to extend and improve the work done on several points that I will explain in time.
The second and third chapters dedicated respectively to the extension of MLF with explicit polymorphism (à la System F), and higher-order types (Fω). I will probably not publish them directly on this blog; of course, a complete PDF should be available eventually.
The implementation part, supposed to correspond closely to the subject of my internship, turned out to be of quite larger scope. Some of the latter parts of Boris Yakobowski’s PhD thesis had not been translated into code, and I was responsible for their integration in the current MLF typer prototype. I also tackled some other aspects of various natures — term and types printing and display, built-in types and values, interactive toplevel — that were present in the former prototypes of both Didier Le Botlan and Boris Yakobowski, but were not up-to-date anymore with the latest presentation of the MLF metatheory.
I will not insist here on the software development and the interesting but delicate software engineering considerations that I had to handle during my internship.
What I will present here is an informal introduction to the subject of my master thesis, MLF. It is only intended to convey a good intuition of MLF and various related formal type systems — eMLF, gMLF, xMLF — and its relation to the well-known systems ML and System F.
ML, System F and MLF
ML as a type system
e ::= ML expressions | x, y, z variables | λ(x) e λ-abstraction | e₁ e₂ application | let x = e₁ in e₂ local definition
ML makes a distinction between two levels of types: monomorphic and polymorphic types — usually named type schemes:
τ ::= ML monotypes | α, β, γ type variables | τ → τ function types σ ::= ML polytypes | τ monorphic type | ∀(α) σ type quantification
For a formal description of the ML type system, typing judgments and derivations, see Milner 78. Informally, the crucial part of the type system is let-polymorphism:
- λ-bound variables get assigned monomorphic types
- let-bound variables get assigned polymorphic types
In other words,
let-definition are the only place in a ML program
where polymorphism is introduced, by generalizing the monorphic type
of the bound term. Of the two following expressions, only the second
(fun x -> x) carries a monorphic type of the
form α→α, wich is distinct from the generalized type scheme ∀(α)α→α
and cannot be used with different values of α.
(fun id -> (id 1, id true)) (fun x -> x) let id = (fun x -> x) in (id 1, id true)
In particular, the typing rule for application is monomorphic: when
typing applications, both the left and right side are assigned
monorphic types. When using a let-bound variable in such a position —
id 1 of the above example — we implicitly choose
a monomorphic instance of its polymorphic type, by replacing each
∀-quantified type variable with a monomorphic type — here the constant
More generally, there is an instance relation between polymorphic types: σ₁ is an instance of σ₂ if we can transform σ₁ into σ₂ by replacing some of its quantified variable by monomorphic types, possibly introducing new free type variables, and finally quantifying over those free variables. For exemple, ∀(β) (int→β) → (int→β) is an instance of ∀(α) α→α.
ML is a very succesful type system, used in practical languages, due to the possibility of principal type inference. There are inference algorithms for ML, based on first-order unification, which have the two desirable properties:
They will decide a correct polymorphic type for every term typable in ML.
The chosen type is principal: every other valid ML type for that term is an instance of this type.
In other words, it is possible to infer, for each typable term, a most general polymorphic type.
Note that the term language of ML does not contain any syntactic construct related to typability and polymorphism: type annotations, etc. ML features implicit polymorphism.
Limitations of ML restricted polymorphism
After using the ML type systems for decades, programmers have become quite accustomed to its limitations. For example, the following term is not typable in ML:
λ(f) (f 0, f true)
(For that example, we have enriched our language with built-in constants and types, and tuples.)
This is not typable because
f cannot be a monorphic function, as it
takes input of different types, integers and booleans.
f could be
the identity function, of type ∀(α) α→α, but that would require
assigning a polymorphic type to a λ-parameter, which is not possible in
ML. However, the following definition is correct:
let f = λ(x) x in (f 0, f true)
This artificial example is in fact representative a deep problem of
software engineering in languages using the ML type system. If
a programmer encounters a program expression e making heavy use of the
f, he cannot necessarily abstract over it:
(λ(f) e) f. If
f is used polymorphically in
e, this abstraction
would break typability: we are not necessarily able to factor out
parts of the program.