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 3: introduction to MLF

(Gabriel Scherer (gasche) @ 2010-11-15 19:45:32)

MLF provides a new way to express equality information inside types. The most general type for choose id, expressing both local polymorphism and subtypes equality, is written:

∀(α ≥ ∀(β)β→β) α → α

A high-level description of MLF types

Such quantification using a ≥-bound is called flexible quantification. We can describe flexible MLF types with the following grammar:

σ ::=                    flexible MLF types
    | α, β, γ            type variables
    | ⊥                  bottom
    | α → β              function types (using only variables)
    | ∀(α ≥ σ₁) σ₂       flexible quantification

Any type is an instance of ⊥, and instances of ∀(α≥σ₁)σ₂ may specialize both σ₁ and σ₂. The usual ML schemes ∀(α)σ can be written ∀(α≥⊥)σ.

Note that the arrow type (and, more generally, any of the traditional constructors of monomorphic types such as tuples) are expressed monomorphically, using only variables. (α→β)→γ is written ∀(δ≥α→β)δ→γ. This presentation does not change expressivity, but helps separating the first-order structure and the polymorphism structure of a term: the only parts relevant for polymorphism are in quantifications, we do not have to look deep into nested arrows to find instantiable subtypes.

This is only useful when the bound actually carry polymorphism. Syntactic sugar can be defined so that "inert" (not further instantiable) bounds such as α→β can be inlined.

For example, we can express both System F types for choose id as instances of ∀(α ≥ ∀(β) β→β) α→α:

∀(β) ∀(α≥β→β) α → α                  loss of local polymorphism
∀(α'≥∀(β)β→β) ∀(α≥∀(β)β→β) α' → α    loss of sharing information

The second type is actually not a faithful transcription of the System F type (∀(β)β→β)→(∀(β)β→β). This System F type can represent terms where the polymorphism of the left-hand side is required. Using MLF flexible bound, we can only express types were polymorphism is available.

Therefore, we add a rigid binding to express required polymorphism:

σ ::=                 MLF types
    | ...             MLF flexible types
    | ∀(α=σ₁) σ₂      rigid quantification

When instantiating a rigid quantification, we may not specialize the bound type σ₁. The System F type can then be expressed:

∀(α'=∀(β)β→β) ∀(α≥∀(β)β→β) α' → α    restricted polymorphism

This type is an instance of the former one: ∀(α≥σ₁)σ₂ can be weakened into ∀(α=σ₁)σ₂. So we have actually used two steps to the System F type: first losing the equality information, then forgetting that the left hand side can still be refined.

MLF and type annotations

As we have seen earlier, to construct terms using higher-order polymorphism, it is necessary to use a certain amount of type annotations in terms. Where are the polymorphism annotations in MLF terms?

The answer is refreshingly simple: polymorphism is made explicit in MLF terms by using constants. Those constants introduce polymorphism in the form of rigid bounds. For each (polymorphic) type σ, we introduce a constant coerce{σ} with the following type:

∀(α=σ) ∀(β≥σ) α → β

Those constants can be considered as coercion functions. When applied to a term, they force the inference algorithm to give a polymorphic type to this term — exactly σ, and not one of its monomorphic instances: this is the role of rigid quantification.

For example, the former type ∀(α'=∀(β)β→β) ∀(α≥∀(β)β→β) α'→α can be constructed with the following term:

λ(x) (coerce{∀(β) β→β} x)

In order to get more familiar-looking annotations, we define the following syntactic sugar:

let x:σ = e₁ in e₂     ⟶     let x = coerce{σ} e₁ in e₂
λ(x:σ) e               ⟶     λ(x) (let x = coerce{σ} x in e)

The former example can then be written simply

λ(x : ∀(β) β→β) x

It took me a while to understand why it is so cool that annotations are only constants. It means that the pre-existing concepts of the MLF type system can already express user-defined annotations, without needing additional machinery. Don’t bother if it seems trivial to you, you will see the light later.

The good properties of MLF

The coercion functions are actually the only part of the MLF type system that introduce rigid quantifications. All types generated during the inference of let bounds, functions and applications use flexible quantification.

We have the two following properties:

  1. The MLF typable terms that do not use coercions are exactly the ML typable terms. In particular, all ML terms are typable in MLF without requiring additional type annotations.

  2. Terms admitting polymorphic types need not be annotated, only function parameters that are used polymorphically need to.

Additionnally, typability of MLF terms is very stable, as it is preserved by a large range of transformations. For example, the following two examples of rewriting preserve the set of typable MLF terms:

e₁ e₂         ⟶      (λ(f) λ(x) f x) e₁ e₂
e₂[x←e₁]      ⟶      let x = e₁ in e₂        (* provided x appears free in e₂ *)
f             ⟶      λ(x) (f x)              (* when f is a function *)

Note in particular that, in the latter example, no annotation is required on x even if f requires a polymorphic type for its parameter: in that case, x is polymorphic but not used polymorphically, it is only passed to a function.