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 4: gMLF, graphical MLF types

(Gabriel Scherer (gasche) @ 2010-11-16 13:20:35)

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.

fig:graph-structure-examples

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.

fig:graph-binding-examples

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:

fig:graph-sharing-examples

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

fig:graph-illformed-examples

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

fig:graph-flag-examples

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 :

We can therefore present gMLF types on the base of the four following components:
  1. the structure tree
  2. the sharing relation
  3. the binding tree
  4. 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 α → ....

fig:graph-bound-alias-examples

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 :

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

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