Une présentation moderne de l’inférence de types pour ML

Types

Une signature Σ est un ensemble T de constructeurs de types, notés T, doté chacun d’une arité entière a(T). On se donne un ensemble de variables de types V. Les types τ sont les éléments de l’algèbre libre engendrée par Σ et V.

Damas-Milner (Damas-Milner) type schemes are given by σ ::= ∀ᾱ.τ.

Var ; \frac{Γ(x) = σ}{Γ ⊢ x : σ}  Abs ; \frac{Γ; x : τ ⊢ e : τ′}{Γ ⊢ λx.e : τ → τ′}  App ; \frac{Γ ⊢ e_{1} : τ → τ′  Γ ⊢ e_{2} : τ}{Γ ⊢ e_{1} e_{2} : τ′}

Let

\frac{Γ ⊢ e_{1} : σ Γ; x : σ ⊢ e_{2} : τ}{Γ ⊢ let x = e_{1} in e_{2} : τ}

\frac{Γ ⊢ e : τ  ᾱ ∩ ftv(Γ) = ∅}{Γ ⊢ e : ∀ᾱ.τ}

Inst \frac{Γ ⊢ e : ∀ᾱ.τ}{Γ ⊢ e : τ[τ̄/ᾱ]}

Gen

Extension du système Pour plus de puissance, on souhaite ajouter une règle de conversion:

Conv ; \frac{Γ ⊢ e : τ τ =_{E} τ′}{Γ ⊢ e : τ′}

voire, plus généralement,

Sub ; \frac{C, Γ ⊢ e : τ C ⊩ τ = τ′}{C, Γ ⊢ e : τ′}

De plus, l’introduction de contraintes permet de décrire le processus d’inférence sous forme agréable (règles de réécriture) et réaliste (modélisation du partage).

Un premier langage de contraintes On se donne des contraintes et des schémas de types contraints:

C ::= true | false | ϵ | C ∧ C | ∃α.C
σ ::= ∀ᾱ[C].τ

Une multi-équation ϵ est un multi-ensemble de types.

Interprétation

Un modèle de Σ est un ensemble M, muni, pour chaque constructeur de type T d’arité n, d’une fonction injective T de M^{n} dans M. Une substitution ground est une fonction totale de V dans M. On l’étend naturellement aux types. On définit alors le prédicat ϕ ⊢ C:

ϕ ⊢ true  \frac{∀τ ∈ ϵ ϕ(τ) = t}{ϕ ⊢ ϵ}  \frac{ϕ ⊢ C_{1}  ϕ ⊢ C_{2}}{ϕ ⊢ C_{1} ∧ C_{2}}  \frac{ϕ[α ↦ t] ⊢ C}{ϕ ⊢ ∃α.C}

Implication (⊩) et équivalence (≡) de contraintes s’en déduisent.

Raisonner sur les contraintes

\frac{C ∧ true}{C}  \frac{∃α.true}{true}  \frac{C ∧ false}{false}  \frac{∃α.false}{false}  \frac{C_{1} ∧ C_{2}}{C_{2} ∧ C_{1}}  \frac{(C_{1} ∧ C_{2}) ∧ C_{3}}{C_{1} ∧ (C_{2} ∧ C_{3})}

\frac{∃α.∃β.C}{∃β.∃α.C}  \frac{(∃α.C_{1}) ∧ C_{2}}{∃α.(C_{1} ∧ C_{2})} α ∉ ftv(C_{2})  \frac{τ}{true}  \frac{α = ϵ ∧ α = ϵ′}{α = ϵ = ϵ′}

\frac{α = α = ϵ}{α = ϵ}  \frac{T τ_{1} … τ_{n} = T τ′_{1} … τ′_{n} = ϵ}{τ_{1} = τ′_{1} ∧ … ∧ τ_{n} = τ′_{n} ∧ T τ_{1} … τ_{n} = ϵ}

\frac{∃α.(α = ϵ)}{ϵ} α ∉ ftv(ϵ) \frac{C[τ/α] ∧ α = τ = ϵ}{C ∧ α = τ = ϵ}

Cette règle est dérivable à partir des précédentes:

\frac{C[τ/α]}{∃α.(C ∧ τ = α)} α ∉ ftv(τ)

Cette règle est valide si le modèle est une algèbre libre:

\frac{T τ̄ = T′ τ̄′ = ϵ}{false} T ≠ T′

La règle d’occur check (non fournie) est valide si le modèle est une algèbre non récursive. L’ensemble de ces règles est complet dans le modèle des types libres finis.

Le système HM(=) Un jugement est valide uniquement s’il met en jeu une contrainte soluble. J’écris C ⊩ ∀ᾱ[D].τ pour C ⊩ ∃ᾱ.D.

Var ; \frac{Γ(x) = σ  C ⊩ σ}{C, Γ ⊢ x : σ}  Abs ; \frac{C, (Γ; x : τ) ⊢ e : τ′}{C, Γ ⊢ λx.e : τ → τ′}

App \frac{C, Γ ⊢ e_{1} : τ → τ′ C, Γ ⊢ e_{2} : τ}{C, Γ ⊢ e_{1} e_{2} : τ′} Let

\frac{C, Γ ⊢ e_{1} : σ C, (Γ; x : σ) ⊢ e_{2} : τ}{C, Γ ⊢ let x = e_{1} in e_{2} : τ}

Gen

\frac{C ∧ D, Γ ⊢ e : τ  ᾱ ∩ ftv(C, Γ) = ∅}{C ∧ ∃ᾱ.D, Γ ⊢ e : ∀ᾱ[D].τ}

Inst \frac{C, Γ ⊢ e : ∀ᾱ[D].τ}{C ∧ D, Γ ⊢ e : τ}

Sub \frac{C, Γ ⊢ e : τ C ⊩ τ = τ′}{C, Γ ⊢ e : τ′} ∃ Intro

\frac{C, Γ ⊢ e : τ  ᾱ ∩ ftv(Γ, τ) = ∅}{∃ᾱ.C, Γ ⊢ e : τ}

Équivalence entre Damas-Milner et HM(=)

Tout jugement Damas-Milner est un jugement HM(=) valide. (Insérer true partout où cela est nécessaire.) Tout jugement HM(=) valide est un jugement Damas-Milner. (Partout où une contrainte C apparaît, appliquer son unificateur le plus général.)

Extrait de la preuve de complétude Comment HM(=) simule-t-il la règle Inst?

Inst ; \frac{⊢ e : ∀α.τ}{⊢ e : τ[τ′/α]} α ∉ ftv(τ′) s.p.d.g.

On écrit

true ⊢ ∀α[true].τ
true ⊢ τ  (instantiation)
τ′ = α ⊢ τ  (affaiblissement)
τ′ = α ⊢ τ[τ′/α]  (conversion)
∃α.(τ′ = α) ⊢ τ[τ′/α]  (∃ Intro)
true ⊢ τ[τ′/α]  (équivalence)

Une version plus dirigée par la syntaxe

VarInst

\frac{Γ(x) = ∀ᾱ[D].τ}{C ∧ D, Γ ⊢ x : τ}

LetGen

\frac{\begin{matrix}C ∧ D, Γ ⊢ e_{1} : τ_{1} & ᾱ ∩ ftv(C, Γ) = ∅ \\ C, (Γ; x : ∀ᾱ[D].τ_{1}) ⊢ e_{2} : τ_{2} \end{matrix}}{C ∧ ∃ᾱ.D, Γ ⊢ let x = e_{1} in e_{2} : τ_{2}}

La règle de généralisation consulte Γ pour déterminer quelles variables sont généralisables et séparer les portions vieille (C) et fraîche (D). Cette dernière, et seule celle-ci, doit être résolue (simplifiée) avant d’être dupliquée.

Que nous manque-t-il?

La description fournie par HM(=) abstrait certains détails importants, en particulier la notion de rang, et exige une alternance entre génération et résolution. On a interprété les contraintes, et déduit des règles d’équivalence, que l’on peut lire comme des règles de résolution. Ne pourrait-on pas interpréter également les jugements, et en déduire d’autres règles, de façon à décrire tout le processus sous cette forme?

Plus de contraintes On étend le langage de contraintes: C ::= … | let x : σ in C | x(τ). L’interprétation est revue en conséquence:

Γ, ϕ ⊢ true  \frac{∀τ ∈ ϵ ϕ(τ) = t}{Γ, ϕ ⊢ ϵ}  \frac{Γ, ϕ ⊢ C_{1}  Γ, ϕ ⊢ C_{2}}{Γ, ϕ ⊢ C_{1} ∧ C_{2}}
\frac{Γ, ϕ[α ↦ t] ⊢ C  α ∉ ftv(Γ)}{Γ, ϕ ⊢ ∃α.C}  \frac{Γ, ϕ ⊢ σ  (Γ; x : σ), ϕ ⊢ C}{Γ, ϕ ⊢ let x : σ in C}
\frac{Γ_{1}, ϕ ⊢ ∃ᾱ.(C ∧ τ = τ′) ᾱ ∩ ftv(τ′) = ∅}{(Γ_{1}; x : ∀ᾱ[C].τ; Γ_{2}), ϕ ⊢ x(τ′)}  \frac{Γ, ϕ ⊢ ∃ᾱ.C}{Γ, ϕ ⊢ ∀ᾱ[C].τ}

Un système purement à base de contraintes

VarInst x(τ) ⊢ x : τ

Abs

\frac{C ⊢ e : τ′}{let x : τ in C ⊢ λx.e : τ → τ′}

App \frac{C ⊢ e_{1} : τ → τ′ C ⊢ e_{2} : τ}{C ⊢ e_{1} e_{2} : τ′}

LetGen

\frac{C_{1} ⊢ e_{1} : τ_{1} C_{2} ⊢ e_{2} : τ_{2}}{let x : ∀V[C_{1}].τ_{1} in C_{2} ⊢ let x = e_{1} in e_{2} : τ_{2}}

Sub \frac{C ⊢ e : τ C ⊩ τ = τ′}{C ⊢ e : τ′}

\frac{C ⊢ e : τ  ᾱ ∩ ftv(τ) = ∅}{∃ᾱ.C ⊢ e : τ}

Weaken \frac{C′ ⊢ e : τ C ⊩ C′}{C ⊢ e : τ}

∃ Intro

Correspondance avec HM(X)

Si fpv(C) = ∅ et si C, Γ ⊢ e : τ est valide dans HM(X), alors il existe C′ telle que C′ ⊢ e : τ et, pour toute solution ϕ de C, on a ϕ, Γ ⊢ C′. Inversement, si C ⊢ e : τ, alors, pour tout Γ tel que fpv(let Γ in C) = ∅, on a let Γ in C, Γ ⊢ e : τ. Ainsi, si fpv(C) = ∅, alors C ⊢ e : τ et C, ∅ ⊢ e : τ sont équivalents.

Présentation dirigée par la syntaxe

⟦x : τ⟧ = x(τ)
⟦λx.e : τ⟧ = ∃α_{1}α_{2}.(τ = α_{1} → α_{2} ∧ let x : α_{1} in ⟦e : α_{2}⟧)
⟦e_{1} e_{2} : τ⟧ = ∃α_{2}.(⟦e_{1} : α_{2} → τ⟧ ∧ ⟦e_{2} : α_{2}⟧)
⟦let x = e_{1} in e_{2} : τ⟧ = let x : ∀α[⟦e_{1} : α⟧].α in ⟦e_{2} : τ⟧

Correction: ⟦e : τ⟧ ⊢ e : τ. Complétude: si C ⊢ e : τ, alors C ⊩ ⟦e : τ⟧.

Raisonner sur les contraintes, bis

\frac{let x : ∀ᾱ[false].τ in C}{false}  \frac{let x : σ in false}{false}

\frac{let x : σ in (C_{1} ∧ C_{2})}{(let x : σ in C_{1}) ∧ C_{2}} x ∉ fpv(C_{2}) \frac{let x : σ in ∃α.C}{∃α.let x : σ in C} α ∉ ftv(σ)

\frac{let x : σ in C[x(τ′)]}{let x : σ in C[∃ᾱ.(C ∧ τ = τ′)]} σ = ∀ᾱ[C].τ (…)

\frac{let x : ∀ᾱ[C_{1}].τ in C_{2}}{(∃ᾱ.C_{1}) ∧ C_{2}} x ∉ fpv(C_{2})

\frac{let x : ∀ᾱ[C_{1} ∧ C_{2}].τ in C_{3}}{C_{1} ∧ let x : ∀ᾱ[C_{2}].τ in C_{3}} ᾱ ∩ ftv(C_{1}) = ∅

\frac{let x : ∀ᾱ[∃β.C_{1}].τ in C_{2}}{let x : ∀ᾱβ[C_{1}].τ in C_{2}} β ∉ ftv(τ)

\frac{let x : ∀ᾱβ[C_{1}].τ in C_{2}}{∃β.let x : ∀ᾱ[C_{1}].τ in C_{2}} β ∉ ftv(C_{2}) ∧ ∃ᾱ.C_{1} détermine β

Critères de diminution du rang

Voici deux conditions suffisantes pour qu’une contrainte C détermine une variable β ∈ ftv(C).

1. C est ∃β̄.(C′ ∧ α = ϵ), où α ∈ ftv(C) \ {β} et β ∈ ftv(ϵ). Tout terme égal à une variable vieille est entièrement vieux.

2. C est ∃β̄.(C′ ∧ β = τ = ϵ), où ftv(τ) ⊆ ftv(C) \ {β}. Toute variable égale à un terme entièrement vieux est vieille.

L’algorithme

L’algorithme est décrit essentiellement en munissant nos règles de réécriture d’une stratégie. Pour définir et implanter celle-ci, une notion de contexte d’évaluation est utile.

E ::= • | E[let x : σ in •] (σ résolu)
| E[C ∧ •] | E[let x : ∀ᾱ[•].τ in C]

On veut une séparation naturelle entre une portion résolue, soumise à des invariants forts, et une portion non résolue, qui peut être arbitraire. On l’obtient naturellement en écrivant E[C].