A graph representation of MLF types, and a simple, efficient

unification algorithm

Didier Rémy, Boris Yakobowski

INRIA Rocquencourt

Why MLF?

ML  System F
Full type inference  Explicitely typed
(Good)  (undecidable type inference)
Outer ∀  Inner (1st class) ∀ (Good)
∀αβ (α → β) → α t → β t  λ(f : ∀α.α → α)(f [int] 1, f [char] ′c′)

MLF ▶ Type all ML programs (type inference) ▶ Encode all System F programs ▶ Annotations on λ-abstractions whose arguments are

polymorphically used (and only them)

Example: type of choose id

System F  MLF
id = λx.x ∀α. α → α  ∀ (α ≥ ⊥) α → α
choose  ∀γ. γ → γ → γ ∀ (γ ≥ ⊥) γ → γ → γ

In System F, two diffent typings:

choose [∀α · α → α] id :  (∀α · α → α) → (∀α · α → α)
Λα · choose [α → α]  (id α): ∀α · (α → α)  → (α → α)

In MLF:

choose id:  ∀ (β = ∀ (α) α → α) β → β (σ_{1})
: ∀ (α) ∀ (β = α → α)  β → β (σ_{2})

σ = ∀ (β ≥ ∀ (α) α → α) β → β is another principal typing.

MLF with syntaxic types

Syntax of types:

Monotypes : τ ::= α | τ → τ′
Polytypes : σ::= τ | ⊥ | ∀ (α ≥ σ) σ′ | ∀ (α = σ) σ′

Translation from the types of System F:

\begin{matrix}[ ; [α] ; ] = & α \\ \begin{matrix}[ \\ [ & ∀α · t & ] \\ ] \end{matrix} = & ∀ (α ≥ ⊥) [ ; [t] ; ] \\ \begin{aligned}[ \\ [ & t_{1} → t_{2} & ] \\ & ] \end{aligned} = & ∀ (α_{1} = \begin{matrix}[ \\ [ & t_{1} & ] \\ & ] \end{matrix}) ∀ (α_{2} = \begin{matrix}[ \\ [ & t_{2} & ] \\ & ] \end{matrix}) α_{1} → α_{2} \end{matrix}

Instance relation

The instance ≺ relation should be as general as possible, while remaining sound and implicit Needed for type inference . But full generality and type inference are incompatible Otherwise, we would get a system as general as System F with decidable type inference .

We split ≺ in two subrelations ⊑ and ⊏ − named instance and abstraction such that :

▶ ≺= (⊑ ∪ ⊐ −)^{⋆} is sound

▶ ⊏ − ⊂ ⊑

▶ ⊑ is implicit

▶ ⊏ − is explicitely reversible (and should be as small as possible)

Equivalence (≡) is the kernel of the instance relation. It deals with commutations of binders, sharing of monotypes, removal of unnecessary binders (∀ (α = σ) α ≡ σ)

Difficulty with the current presentation

▶ Canonical form w.r.t the equivalence relation cannot be preserved by abstraction and instance. Equivalence 6 non-trivial rules shows up during proofs.

▶ The abstraction 4 rulesand instance 6 rules relations are defined by purely syntactic means, without much support for intuition. They are only justified by the properties of MLF.

Contributions

▶ Graphs have already been proposed as a simpler representation for types, but were not formalized

▶ Complexity of the unification algorithm is unknown

▶ Reasoning about MLF is heavy Didier Le Botlan’s PhD thesis is 320 pages longs , even though the presentation is not that complicated

MLF with graphs

Types are represented by graphs. More precisely, a dag structure represents the skeleton of the type, and a tree the binding structure.

               σ = (int → float) → (int → float)

→

→
int  float

σ′ = ∀ (α ≥ ⊥) ∀ (β = ∀ (γ ≥ ⊥) γ → α) β → β ; \begin{aligned}& & & → \\ & → & β \\ _{⊥ _{γ}} & & & _{⊥ _{α}} \end{aligned}

MLF with graphs

Types are represented by graphs. More precisely, a dag structure represents the skeleton of the type, and a tree the binding structure.

              σ = (int → float) → (int → float)

→

→
int  float

σ′ = ∀ (α ≥ ⊥) ∀ (β = ∀ (γ ≥ ⊥) γ → α) β → β ; \begin{aligned}& & & → \\ & → & β \\ _{⊥ _{γ}} & & & _{⊥ _{α}} \end{aligned}

Translation from syntaxic graphs

▶ Translation of monotypes is straightforward ▶ Translation of ∀ (α = σ) σ′ is inductively defined.

(same for flexible bounds)

1. Convert σ to G.

2. Convert σ′ to G′. α is a free variable of σ′, and appears as a free node in G.

3. Join G and G′.

4. Bind the node corresponding to α to the

root of G′ (if there is polymorphism in G).

G G′ α G

Induce some well-formedness conditions for the binding graph.

Equivalence of graphs

Equivalence on graphs is only sharing or unsharing of monomorphic nodes.

\begin{matrix}→ \\ → \\ → \\ int & ⊥ \end{matrix}  ≡  \begin{matrix}→ \\ → \\ → & → \\ int & & ⊥ \end{matrix}

Equivalent syntaxic types are translated to equivalent graphs, and reciprocally.

Instance on graphs: Inst rule

The Inst rule allows to replace a ⊥ node by a new graph. It is similar to the standard ML rule for instantiation, except it can introduce more polymorphism.

\begin{aligned}& & list \\ & & → \\ & → & & ⊥ \\ int & ⊥ \end{aligned}

⊑

list

→

→  →

int  ⊥  int  ⊥

Instance on graphs: Merge rule

The Merge rule allows to merge together two subgraphs bound to the same node which are identical.

list →

→  →
int  ⊥  int  ⊥

⊑

\begin{aligned}& list \\ & → \\ & → \\ int & ⊥ \end{aligned}

Instance on graphs: Extrude rule

The Extrude rule permits to lift a binder on top of another. This decreases the rank of the polymorphism of the type.

Instance on graphs: Rigid rule

A flexible binder can be turned into a rigid one through the Rigid rule.

Restrictions to instance

Instantiation through any of the previous rules can only happen on nodes which are at a flexible path from the root of the graph. Instantiation under a rigid bound is forbidden.

\begin{aligned}& list \\ & → \\ & → \\ int & ⊥ \end{aligned}

⋢

\begin{aligned}& list \\ & → \\ & → \\ int & ⊥ \end{aligned}

⋢

list

→

→

int  float

Instance: properties

Instance also includes Abstraction, which permits Merge and Extrude for nodes which are at a path allowing abstraction.

⇒ Instance includes exactly 6 different rules, which can be seen as conditional rewriting steps on graphs.

Instance on graphs and instance on syntaxic types permit to derive the same judgments (w.r.t the conversion functions).

Rules of an instance derivation can be ordered:

1. All Inst steps

2. All Extrude steps

3. Merge and Rigid intermingled

Unification algorithm

Given G_{1} and G_{2}, we want to find the most general graph G such that G_{1} ⊑ G and G_{2} ⊑ G.

1. First-order unification of the structure graph of G_{1} and G_{2}. Gives the skeleton S of G.

2. Bind the nodes of S, using the binders of G_{1} and G_{2}. This gives a possible G.

3. Check that G is indeed an instance of G_{1} and G_{2} (in fact, only the uses of the Merge rules). If not, there is no unifier.

Unification: properties

▶ Sound algorithm (always returns an instance of G_{1} and G_{2}) ▶ We are currently proving principality ▶ Good complexity: linear in the sizes of the input graphs. ▶ For ML types, the algorithm simplifies to the standard

1st-order unification algorithm.

Conclusion

▶ More readable types ▶ Simpler proofs and rules ▶ Presentation more intuitive Rules are what one would expect on graphs and more canonical ▶ Complexity of the unification algorithm is now known