## A long story about MLF, part 3: introduction to MLF

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:

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.

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.