A long story about MLF
  1. A long story about MLF, part 1: Introduction, ML
  2. A long story about MLF, part 2: System F and principality
  3. Moderately practical uses of System F over ML
  4. A long story about MLF, part 3: introduction to MLF
  5. A long story about MLF, part 4: gMLF, graphical MLF types

A long story about MLF, part 1: Introduction, ML

(Gabriel Scherer (gasche) @ 2010-10-27 16:53:41)

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

We’re interested in ML as a type system, so we will keep the term-level complexity of the language minimal:

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:

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 typechecks, because (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 — such as id in 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 type int.

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:

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 variable 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.