Inférence de types à base de contraintes

François Pottier – INRIA Rocquencourt

              Francois.Pottier@inria.fr

Aperçu

• Typage et inférence en présence de contraintes

• Application aux enregistrements

• Résolution et simplification de contraintes λ-calcul simplement typé Syntaxe:

e ::= x | λx.e | e e  (termes)
t ::= ι | t → t  (types ground)
G ::= • | G; x : t  (environnements ground)

Règles:

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

François Pottier, INRIA  3  novembre 2001

λ-calcul simplement typé: inférence Syntaxe:

τ ::= α | ι | τ → τ  (types)
C ::= true | C ∧ C | ∃α.C | τ = τ  (contraintes)
Γ ::= • | Γ; x : τ  (environnements)

À tout pré-jugement Γ ⊢ e : τ on associe une contrainte ⟦Γ ⊢ e : τ⟧, dont les variables libres sont (au plus) celles de Γ et τ, définie par:

⟦Γ ⊢ x : τ⟧ = Γ(x) = τ  (var)
⟦Γ ⊢ λx.e : τ⟧ = ∃αβ.(⟦Γ; x : α ⊢ e : β⟧ ∧ α → β = τ) (abs)
⟦Γ ⊢ e_{1} e_{2} : τ⟧ = ∃α.(⟦Γ ⊢ e_{1} : α → τ⟧ ∧ ⟦Γ ⊢ e_{2} : α⟧) (app)

Convention de Barendregt: α et β sont pris distincts et non libres dans Γ ou τ; on écrit αβ # Γ, τ.

François Pottier, INRIA  4  novembre 2001

Exemple Création des contraintes:

⟦0 : int ⊢ (λx.x) 0 : α⟧

= ∃β.(⟦0 : int ⊢ λx.x : β → α⟧ ∧ ⟦0 : int ⊢ 0 : β⟧)
= ∃β.(∃γδ.(⟦0 : int; x : γ ⊢ x : δ⟧ ∧ γ → δ = β → α) ∧ int = β)
= ∃β.(∃γδ.(γ = δ ∧ γ → δ = β → α) ∧ int = β)

Résolution:

∃β.(∃γδ.(γ = δ ∧ γ → δ = β → α) ∧ int = β)
≡ ∃β.(∃γδ.(β = γ = δ = α) ∧ int = β)
≡ ∃β.(int = β = α)
≡ int = α

Interprétation des contraintes Une substitution ρ associe à toute variable α un type ground t. On définit alors la relation de satisfaction:

ρ ⊢ true  \frac{ρ ⊢ C_{1}  ρ ⊢ C_{2}}{ρ ⊢ C_{1} ∧ C_{2}}  \frac{ρ[α ↦ t] ⊢ C}{ρ ⊢ ∃α.C}  \frac{ρ(τ_{1}) = ρ(τ_{2})}{ρ ⊢ τ_{1} = τ_{2}}

et la relation d’implication:

\frac{∀ρ ρ ⊢ C_{1} ⇒ ρ ⊢ C_{2}}{C_{1} ⊩ C_{2}}

Deux contraintes sont équivalentes (C_{1} ≡ C_{2}) ssi elles s’impliquent mutuellement (C_{1} ⊩ C_{2} ∧ C_{2} ⊩ C_{1}). λ-calcul simplement typé avec sous-typage On se donne une relation d’ordre ≤ sur les types ground vérifiant la propriété:

t_{1} → t_{2} ≤ t′_{1} → t′_{2} ⟺ t′_{1} ≤ t_{1} ∧ t_{2} ≤ t′_{2}

On introduit alors une règle non dirigée par la syntaxe:

Sub ; \frac{G ⊢ e : t t ≤ t′}{G ⊢ e : t′}

François Pottier, INRIA  7  novembre 2001

λ-calcul simplement typé avec sous-typage: inférence On introduit une nouvelle forme de contraintes:

C ::= … | τ ≤ τ (contraintes)

interprétée de façon immédiate:

\frac{ρ(τ_{1}) ≤ ρ(τ_{2})}{ρ ⊢ τ_{1} ≤ τ_{2}}

La règle (var) est modifiée comme suit:

⟦Γ ⊢ x : τ⟧ = Γ(x) ≤ τ (var)

Exemple Création des contraintes:

⟦0 : int ⊢ (λx.x) 0 : α⟧

= ∃β.(⟦0 : int ⊢ λx.x : β → α⟧ ∧ ⟦0 : int ⊢ 0 : β⟧)
= ∃β.(∃γδ.(⟦0 : int; x : γ ⊢ x : δ⟧ ∧ γ → δ = β → α) ∧ int ≤ β)
= ∃β.(∃γδ.(γ ≤ δ ∧ γ → δ = β → α) ∧ int ≤ β)

Résolution:

∃β.(∃γδ.(γ ≤ δ ∧ γ → δ = β → α) ∧ int ≤ β)
≡ ∃β.(∃γδ.(β = γ ≤ δ = α) ∧ int ≤ β)
≡ ∃β.(int ≤ β ≤ α)
≡ int ≤ α

λ-calcul avec let et sous-typage Syntaxe:

e ::= … | let x = e in e  (termes)
σ ::= ∀ᾱ[C].τ  (schémas de types)
Γ ::= • | Γ; x : σ  (environnements)

Règles dirigées par la syntaxe:

Var ; \frac{Γ(x) = σ}{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} : τ}

François Pottier, INRIA  10  novembre 2001

λ-calcul avec let et sous-typage, suite Règles non dirigées par la syntaxe:

Sub \frac{C, Γ ⊢ e : τ C ⊩ τ ≤ τ′}{C, Γ ⊢ e : τ′} ∀ Intro

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

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

\frac{C, Γ ⊢ e : σ  ᾱ # Γ, σ}{∃ᾱ.C, Γ ⊢ e : σ}

Weaken

\frac{C, Γ ⊢ e : σ C′ ⊩ C}{C′, Γ ⊢ e : σ}

François Pottier, INRIA  11  novembre 2001

λ-calcul avec let et sous-typage: inférence On étend (var) et on introduit (let):

⟦Γ ⊢ x : τ′⟧ = ∃ᾱ.(C ∧ τ ≤ τ′)
si Γ(x) = ∀ᾱ[C].τ  (var)
⟦Γ ⊢ let x = e_{1} in e_{2} : τ⟧ = ∃α.⟦Γ ⊢ e_{1} : α⟧
∧ ⟦Γ; x : ∀α[⟦Γ ⊢ e_{1} : α⟧].α ⊢ e_{2} : τ⟧ (let)

Convention de Barendregt: ᾱ # τ′ pour (var), α # Γ pour (let).

(abs) et (app) restent inchangées.

Propriétés formelles Auto-réduction et sûreté du typage (subject reduction et progress); correction et complétude de l’algorithme d’inférence.

Le système HM(X) – Sulzmann, Odersky, Wehr, 1999 On peut ajouter de nouvelles formes de contraintes et/ou interpréter les contraintes dans d’autres modèles (e.g. set constraints). On peut ajouter des opérations primitives au langage, dotées de règles de réduction appropriées, pourvu que les propriétés d’auto-réduction et de sûreté soient préservées.

Enregistrements naïfs Les types enregistrements sont de la forme {F } où F est une fonction partielle (finie) des labels vers les types. On définit {F } ≤ {F′} par

∀l ∀τ′ F′(l) = τ′ ⇒ ∃τ F (l) = τ ∧ τ ≤ τ′

Opérations exprimables:

• Création: e.g. {x = 1; y = true} : {x : int; y : bool}.

• Accès: .x a le type ∀αβ[α ≤ {x : β}].α → β, que l’on peut également écrire ∀β.{x : β} → β.

L’opération d’extension n’est pas exprimable: e.g. {} → {x : int}, {y : bool} → {y : bool; x : int}, etc. ne sont pas instances d’un unique schéma.

Enregistrements avec rangées – Wand, Rémy Les types enregistrements sont de la forme {ρ} où ρ est une rangée:

ρ ::= α | l : τ; ρ | ∂τ (rangées)

Une rangée représente une fonction totale des labels vers les types, d’où nécessité d’introduire deux constructeurs de types supplémentaires, Abs et Pre. On les munit de la relation Pre τ ≤ Abs.

• Accès: .x a pour type ∀αφ.{x : Pre α; φ} → α.

• Extension: +x a pour type ∀φψα.{x : φ; ψ} → α → {x : Pre α; ψ}.

• Enregistrement vide: {} a pour type {∂Abs}.

• Création: exprimable en fonction des deux précédents; e.g. {x = 1; y = true} : {x : Pre int; y : Pre bool; ∂Abs}.

Notons que le rôle du sous-typage est largement diminué dans ce contexte.

François Pottier, INRIA  15  novembre 2001

Une opération complexe: la concaténation d’enregistrements Si l’on représente un enregistrement par une fonction (totale) des labels vers les champs:

f ::= Abs | Pre v (champs)

alors la concaténation est décrite, champ par champ, par deux règles:

f_{1} @ Abs se réduit vers f_{1}
f_{1} @ (Pre v_{2}) se réduit vers Pre v_{2}

Concaténation, suite Pour décrire cette opération, la relation Pre τ ≤ Abs est inadaptée,

car on attend (Pre bool) @ Abs = Pre bool (types)
mais on a (Pre true) @ (Pre 0) → Pre 0 (valeurs)

Il faut donc un langage de types plus raffiné. On introduit un troisième constructeur Either, et on définit la relation de sous-typage par

Abs ≤ Either τ
Pre τ ≤ Either τ′ ssi τ ≤ τ′

Abs et Pre sont maintenant incomparables.

Concaténation, fin On peut alors donner à l’opération de concaténation un schéma de types qui en décrit fidèlement la sémantique, à condition de se doter de contraintes conditionnelles: Sémantique (rappel):

f_{1} @ Abs se réduit vers f_{1}
f_{1} @ (Pre v_{2}) se réduit vers Pre v_{2}

Schéma de types:

@ : ∀φ_{1}φ_{2}φ_{3}α_{2}[C].{φ_{1}} → {φ_{2}} → {φ_{3}}
où C est  φ_{2} ≤ Either α_{2}
∧ if Abs ≤ φ_{2} then φ_{1} ≤ φ_{3}
∧ if Pre ≤ φ_{2} then Pre α_{2} ≤ φ_{3}

Contraintes conditionnelles Syntaxe:

C ::= … | if h ≤ τ then τ ≤ τ (contraintes)

Interprétation:

\frac{h ≤ head(ρ(τ)) ⇒ ρ ⊢ τ_{1} ≤ τ_{2}}{ρ ⊢ if h ≤ τ then τ_{1} ≤ τ_{2}}

François Pottier, INRIA  19  novembre 2001

Résolution de contraintes On la décrit en général par un système de règles de réécriture. On prouve que le système termine, qu’il préserve l’espace des solutions, et que toute forme normale (dite résolue) admet une solution. Exemples de règles:

• Fusion: τ = α ∧ α = τ′ produit τ = τ′;

• Transitivité: τ ≤ α ∧ α ≤ τ′ produit τ ≤ τ′;

• Décomposition: τ_{1} → τ_{2} ≤ τ′_{1} → τ′_{2} produit τ′_{1} ≤ τ_{1} et τ_{2} ≤ τ′_{2};

• Commutation: (x : τ_{1}; τ_{2}) ≤ (y : τ′_{1}; τ′_{2}) produit ∃φψφ′ψ′.(τ_{2} = (y : φ; ψ) ∧ τ′_{2} = (x : φ′; ψ′) ∧ τ_{1} ≤ φ′ ∧ φ ≤ τ′_{1} ∧ ψ ≤ ψ′);

• Déclenchement: if Pre ≤ Pre τ then τ_{1} ≤ τ_{2} est remplacée par τ_{1} ≤ τ_{2};

• Non-déclenchement: if Pre ≤ Abs then τ_{1} ≤ τ_{2} est supprimée;

• Erreur: int = bool, Either τ ≤ Abs, etc. conduisent à un échec.

Simplification de contraintes: polarités On se place dans le cadre de contraintes de sous-typage non atomiques (⊥ ≤ τ → τ′ ≤ ⊤). On veut simplifier un schéma clos ∀[C].τ_{0}, où C est résolue et sans ∃. On calcule la polarité de chaque variable, par point fixe, d’après les règles suivantes (règles symétriques omises):

τ_{0}^{+}  \frac{(τ_{1} → τ_{2})^{+}}{τ_{1}^{−}  τ_{2}^{+}}  \frac{τ ≤ α  α^{+}  τ n’est pas une variable}{τ^{+}}

Informellement, l’assertion α^{+} indique que α représente le type d’un résultat; α risque alors de recevoir de nouvelles bornes supérieures à l’avenir. On peut faire en sorte qu’aucune variable soit à la fois positive et négative.

Simplification de contraintes: garbage collection Une fois les polarités connues, on peut se contenter de conserver les contraintes de la forme

• α^{−} ≤ β^{+};

• α^{−} ≤ τ^{−} et τ^{+} ≤ α^{+}; où τ n’est pas une variable. Par exemple,

de int ≤ δ ≤ int ∧ γ_{0}^{−} → γ_{1}^{+} ≤ α^{−} ≤ β ≤ γ^{+}
on ne conserve que γ_{0}^{−} → γ_{1}^{+} ≤ γ^{+} ∧ α^{−} ≤ γ^{+}

Simplification de contraintes: canonisation Une conjonction

α_{1} → α_{2} ≤ γ ∧ β_{1} → β_{2} ≤ γ

peut être réduite en

∃γ_{1}γ_{2}.((γ_{1} → γ_{2} ≤ γ) ∧ (α_{2}, β_{2} ≤ γ_{2}) ∧ (γ_{1} ≤ α_{1}, β_{1}))

Cela correspond essentiellement à la règle (α_{1} → α_{2}) ⊔ (β_{1} → β_{2}) = (α_{1} ⊓ β_{1}) → (α_{2} ⊔ β_{2})

On se ramène ainsi à une seule borne construite par variable.

Simplification de contraintes: minimisation On peut définir une notion d’équivalence entre variables, qui rappelle l’équivalence entre états d’un automate fini. On peut appliquer l’algorithme de Hopcroft pour calculer cette relation et identifier les variables équivalentes. Par exemple, si la contrainte est

α^{−} ≤ F α^{−} ∧ β^{−} ≤ F β^{−}

pour un certain contexte F, alors on peut identifier α et β.

Simplification de contraintes, fin Si une variable non-positive admet exactement une borne supérieure, alors on peut les identifier. Par exemple, les schémas ∀αβ[α^{−} ≤ {x : β^{±}}].α^{−} → β^{±} et ∀β.{x : β^{±}} → β^{±} sont équivalents. Simplification souhaitable pour l’affichage, mais détruit certains invariants (petits termes et absence de variables ±).

Conclusion L’inférence à base de contraintes est une technique intéressante, mais:

• est difficile à implanter efficacement (en présence de sous-typage);

• pose encore certains problèmes théoriques (équivalence entre schémas);

• produit des types parfois difficiles à interpréter pour l’utilisateur.