## A long story about MLF, part 4: gMLF, graphical MLF types

## gMLF: Graphical MLF types

The formal definition of MLF syntactic types, instance relations, unification and inference algorithms are the main result of Didier Le Botlan’s PhD thesis. They have proved very technical and difficult to get right. Furthermore, the resulting unification algorithm is not very efficient. Extending the type system with richer features also involved a large amount of work.

Intuitively, one of the reason why the metatheory of syntactical MLF types is so technical is the rich equivalence relation between types. For example, ∀(α≥σ)α is equivalent to σ, and the syntactical unification algorithm needs to be aware of it, burdening its description and correctness proof.

Boris Yakobowski’s PhD thesis develops a new approach of MLF
types. The idea is that, as the MLF quantifications are used to
represent *sharing* information between subtypes, an appropriate
representation for such types may not be a syntactic tree, but
a *graph*. The graphical representation was not new, as it is
informally used in Didier Le Botlan’s thesis, but Boris gave it
a formal status that led to a new, simplified and more maintainable
definition of the MLF type system, named gMLF, which enables an
efficient inference algorithm.

### Graphical types

As we have noted earlier, MLF types provide a clean separation between the monomorphic structure and the polymorphic binders of a type.

Graphic types preserve this separation. A graphic type is the
superposition of two layers, the *structure graph* and the *binder
tree*.

The structure graph is a tree with shared nodes, which describes the monomorphic structure of the term.

The binding tree is given by an arrow for each structure node, that
goes *up* in the structure graph. They correspond to the variable
scope. It is a tree because only one arrow can leave from a given
node.

In syntaxic types, we need variables to express sharing. The rich quantification of MLF was introduced to express sharing between arbitrary types, not leaf type variables. In a gMLF graph, this is very naturally expressed:

Note that there are restrictions on the binding arrow positions. I will not describe precisely the well-formedness condition, wich is too technical for this document, but instead give two representative examples of ill-formed graphs. In the first case, a binding arrow is "too low" : must be higher than any structure edge referring to the node content. In the second case, a "well-bracketing" condition is broken, as two binders "intersect".

Finally, we use another kind of binding arrow to represent rigid flags.

As you may have noticed, variable names are not useful anymore in gMLF
graphs : the binding arrow position is enough to indicate the scope of
a quantifier. Therefore, we use only `(⊥)`

.

We may also notice that the structure graph can be decomposed in two separate components :

- a structure
*tree*, without sharing - a
*sharing*relation between nodes

- the structure tree
- the sharing relation
- the binding tree
- the flag binding association

When transformed into a formal definition of gMLF types, this presentation allows to handle each aspect separately during formal developments. It has been developped in more recent works, to appear.

### Graphic types and the bound aliasing problem

It is interesting to compare syntactic and graphic types, and in particular the differences between syntactic quantifiers and binding arrows. It is interesting, because it is not a perfect fit : while we gained the ability to express sharing, we also lost some precision : there are particularities of syntactic types that cannot be expressed in the graph model.

For example, consider the type `∀(α) int`

: it has no direct graphical
representation. The problem is that we cannot represent the ∀(α)
quantification by a binding arrow, as we wouldn’t know where to place
it: as `α`

is not used in the type, there is no structure node
corresponding to α.

We also lost the ability to distinguish `∀(α)∀(β)σ₁→σ₂`

and
`∀(β)∀(α)σ₁→σ₂`

. In both cases, the arrows for `α`

and `β`

will point
to the (→) node at the top of the graph. Binding arrows are unordered.

Those two differences can be seen as the strength of the graphic
model. When doing type inference, we do not care about unusued type
variables or quantifier ordering. In fact we do not *want* to care
about it : the less the inference algorithm is burdened with such
details, the better.

However, we must keep in mind that there may be mismatch between the syntactic and the graphic types. The user is familiar with the behavior of syntactic types, and may be sadly surprised if she was confronted to such differences.

There is a third important difference between syntactic and graphic
types, which is probably the most problematic. How is the type ```
∀(α≥⊥)
α → ∀(β≥α) σ
```

represented ? In general, for example with the type
`∀(α) α → ∀(β≥σ₁)σ₂`

, there is no specific difficulty : `α`

is
represented by a `(⊥)`

node bound to the top, and `β`

is an arrow from
the top node of `(σ₁)`

to the (→) node corresponding to `α → ...`

.

But in the special case where σ₁ is itself a variable such as `α`

, we
have a problem : how could we add a binding arrow from α to the (→)
node, when α is already bound at the top of the type ?

In other words, we have a problem because we have two different type variables that denote exactly the same type. That makes two different binding arrows that want to have the same source node, which is not possible.

This is called the *bound aliasing problem*. There are two simple ways
to solve it, neither of them entirely satisfactory :

Raise a type error in case of bound aliasing: the user has to be careful.

Choose one of the arrows, and forget the other. For the result to be well-formed, we must choose the arrow bound the highest. In our example, it’s

`α`

. If we drop the β quantification, we get the following type :`∀(α) α → σ[β←α]`

. The user may be surprised.

This bound alias problem is particularly frustrating because of the
discontinuity it creates inside types : not all types are equal. We
may be perfectly fine using `unit → α`

in a quantification, but
changing it to `α`

instead may deeply disturb the resulting type.

This problem has been constantly present during my internship. It can create special cases that can make reasoning, proofs, or even direct intuition harder. Of course, the type inference engine will not be concerned by the bound alias problem : it will infer correct types, without aliased bounds. It becomes problematic when we give the user to express some types herself, instead of letting the inference engine guess them: it is dangerous for explicit polymorphism. Unfortunately, this is precisely the subject of my internship.