Inférence de type

Planche : 1

Inférence de type

Planche : 2

A: Typage implicite.
B: Inférence de type.
C: Unification.

Planche : 3

Types implicites

Il est très pénible de devoir écrire

Fun (x:Nat) -> x+1

Fun (x:Nat) -> Fun (y:Nat) -> x+y

Alors que les types sont ici « évidents ». Si on écrit

Fun x -> x+1

Fun x -> Fun y -> x+y

Il est clair que l’on peut facilement deviner que x et y doivent être de type Nat.

On peut ensuite vérifier le typage comme il y a quinze jours.

Planche : 4

Typage implicite (à la Curry)

On préfère deviner et vérifier en même temps.

Les règles,

E ⊕ [x:A] ⊢ t:B

E ⊢ (Fun (x:A) -> t):A -> B

E ⊕ [x:A] ⊢ t:A

E ⊢ (Fix (x:A) -> t):A

deviennent

E ⊕ [x:A] ⊢ t:B

E ⊢ (Fun x -> t):A -> B

E ⊕ [x:A] ⊢ t:A

E ⊢ (Fix x -> t):A

Et c’est tout !

Planche : 5

Pour être complet

Voici les autres règles qui ne changent pas.

E ⊢ n:Nat

E(x) = A

E ⊢ x:A

E ⊢ t₁:Nat E ⊢ t₂:Nat

E ⊢ t₁ op t₂:Nat

E ⊢ t₁:Nat E ⊢ t₂:A E ⊢ t₃:A

E ⊢ Ifz t₁ Then t₂ Else t₃:A

E ⊢ t₁:A -> B E ⊢ t₂:A

E ⊢ t₁ t₂:B

E ⊢ t₁:A E ⊕ [x:A] ⊢ t₂:B

E ⊢ Let x = t₁ In t₂:B

En effet, il n’y a rien à deviner ici (cf. le Let).

Planche : 6

Une vraie relation

Contrairement au typage explicite (à la Church).

On peut avoir E ⊢ t:A₁ et E ⊢ t:A₂ pour A₁ ≠ A₂.

Par ex.

[x:Nat] ⊢ x:Nat

⊢ (Fun x -> x):Nat -> Nat

[x:Nat -> Nat] ⊢ x:Nat -> Nat

⊢ (Fun x -> x):(Nat -> Nat) -> Nat -> Nat

Et à vrai dire, pour tout type A, on a facilement

[x:A] ⊢ x:A

⊢ (Fun x -> x):A -> A

Planche : 7

Exemple

Fun x -> x+1 est bien de type Nat -> Nat.

[x:Nat] ⊢ x:Nat [x:Nat] ⊢ 1:Nat

[x:Nat] ⊢ x+1:Nat

⊢ (Fun x -> x+1):Nat -> Nat

On cherche à typer la fonction.
On devine le bon type pour x (Nat).
On cherche à typer x+1.
On type les arguments de l’addition.
On vérifie l’addition.
On construit le type de la fonction.

Mais il y a encore une étape magique : deviner [x:Nat].

Planche : 8

Variable de type

Fun x -> x+1 est de type ? X -> Nat, avec [X=Nat].

[x:X] ⊢ x:X [x:X] ⊢ 1:Nat

[x:X] ⊢ x+1:Nat, [X=Nat]

⊢ (Fun x -> x+1):X -> Nat, [X=Nat]

On cherche à typer la fonction.
On pose que le type de x est X
On cherche à typer l’addition.
Premier argument, second argument.
Pour typer d’addition il faut [X=Nat].
On type la fonction.

Planche : 9

Idée générale de l’inférence (synthèse) de type

Procéder à un essai de vérification, en
- Introduisant des variables,
  E ⊕ [x:X] ⊢ t:A
  
  E ⊢ (Fun x -> t):X -> A
- Et posant des équations.
  E ⊢ t₁:A₁ E ⊢ t₂:A₂
  
  E ⊢ t₁ + t₂:Nat, [A₁ = Nat, A₂ = Nat]
À la fin, on a un type contenant des variables et des équations.

Planche : 10

Retour sur la vérification

Les types sont donc changés, ils peuvent contenir des variables.

Nat ∈ T

X ∈ T

A₁ ∈ T A₂ ∈ T

A₁ -> A₂ ∈ T

Avec les nouveaux types on a :

[x:X] ⊢ x:X

⊢ (Fun x -> x):X -> X

Quel sens donner à un tel type ?

id:X -> X veut dire que id:A -> A pour tout type A.

Et en effet on peut donner les types suivants à Fun x -> x.

Nat -> Nat, (Nat -> Nat) -> Nat -> Nat, etc.
Et même (Y -> Z) -> Y -> Z, mais pas Y -> Nat.

Planche : 11

Variables dans les types

Sémantique :

Si X apparaît dans A, type de t, alors [X↦ B]A est aussi un type de t pour tout type B.

Note : [X↦ B] est une nouvelle notation pour la substitution, cette fois appliquée aux types.

Rappels/Remarques.

Substitution : fonction des variables dans les termes.
Facilement, étendue aux termes : σ(A -> B) = σ(A) -> σ(B).
Substitutions de support fini { X ∣ σ(X) ≠ X }.
Pas de problèmes de capture ici.

Planche : 12

Un sens pour les variables de type

Si X apparaît dans A, type de t, alors [X↦ B]A est aussi un type de t pour tout type B.

Définition justifiée par le lemme (facile).

Soit σ une substitution, alors E ⊢ t:A ⇒ σ(E) ⊢ t:σ(A).
(Avec bien entendu σ(E) défini comme associant σ(E(x)) à x.)

Planche : 13

Autre exemple d’inférence

[f:F, x:X] ⊢ f:F [f:F, x:X] ⊢ x:X

[f:F, x:X] ⊢ f x:Y

[f:F, x:X] ⊢ x:X

[f:F, x:X] ⊢ f x+x:Nat

[f:F] ⊢ (Fun x -> f x+x):X -> Nat

⊢ (Fun f -> Fun x -> f x+x):F -> X -> Nat

On cherche à typer les deux Fun
On cherche à typer f x+x, puis l’application f x.
On a maintenant le type de toutes les feuilles.
Le type de f x est Y avec l’équation [F = X -> Y].
Le type de f x+x est Nat, avec [Y = Nat, X=Nat].
Type final, avec les équations [F = X -> Y, Y = Nat, X=Nat].

Planche : 14

Résultat de l’inférence

Le type :

⊢ (Fun f -> Fun x -> f x+x):F -> X -> Nat

Avec les équations :

[F = X -> Y, Y = Nat, X=Nat]

On résout (en substituant X et Y par leurs valeurs) :

[X ↦ Nat,Y ↦ Nat, F ↦ Nat -> Nat]

On substitue dans le type :

⊢ Fun f -> Fun x -> f x+x:(Nat -> Nat) -> Nat -> Nat

Nous allons systématiser l’algorithme d’inférence de type.

Planche : 15

Production des équations (et du type)

À un environnement de typage E et un terme t, on associe un type A et un ensemble (une liste, peu importent les doublons) d’équations.

E ⊢ t ↝ A, E

Avec les notations de définition de prédicat par induction.

E(X)=A

E ⊢ x ↝ A, ∅

E ⊢ t₁ ↝ A₁, E₁ E ⊢ t₂ ↝ A₂, E₂

E ⊢ t₁ t₂ ↝ X, E₁ ⋃ E₂ ⋃ [A₁ = A₂ -> X]

(X frais)

E ⊕ [x:X] ⊢ t ↝ A, E

E ⊢ (Fun x -> t) ↝ X -> A, E

(X frais)

Planche : 16

Production des équations II

Les opérations sur les entiers.

E ⊢ n ↝ Nat, ∅

E ⊢ t₁ ↝ A₁, E₁ E ⊢ t₂ ↝ A₂, E₂

E ⊢ t₁ op t₂ ↝ Nat, E₁ ⋃ E₂ ⋃ [A₁=Nat, A₂=Nat]

E ⊢ t₁ ↝ A₁, E₁ E ⊢ t₂ ↝ A₂, E₂ E ⊢ t₃ ↝ A₃, E₃

E ⊢ Ifz t₁ Then t₂ Else t₃ ↝ A₂, E₁ ⋃ E₂ ⋃ E₃ ⋃ [A₁=Nat, A₂=A₃]

Planche : 17

Équations III

E ⊕ [x:X] ⊢ t ↝ A, E

E ⊢ (Fix x -> t) ↝ A, E ⋃ [X=A]

(X frais)

E ⊢ t₁ ↝ A₁, E₁ E ⊕ [x:A₁] ⊢ t₂ ↝ A₂, E₂

E ⊢ (Let x = t₁ In t₂) ↝ A₂, E₁ ⋃ E₂

La relative complexité des notations cache un peu que l’on définit en fait une fonction :

Arguments : E et t.
Résultat : la paire (A,E).
Technique : induction sur la structure de t.

Planche : 18

Exemple

À typer Fun f -> 2+f 1.

Type : F -> Nat.

Équations : [F = (Nat -> Y), Y=Nat, Nat=Nat].

Solution : [Y↦Nat, F↦(Nat -> Nat)].

Type : (Nat -> Nat) -> Nat.

Planche : 19

Résoudre

Équations du type E = { A₁=B₁, …, A_n=B_n }, avec un langage de termes simple (sans variables liées).

Une solution : une substitution σ tq, σ(A_i) = σ(B_i). On note les substitutions :

[X₁↦C₁,…,X_m↦C_m]

Et on impose des X_i distincts, tq. X_i n’apparaît dans aucun C_j (substitution idempotente σ ∘ σ = σ).

Retour sur l’exemple : [F = Nat -> Y, Y=Nat, Nat=Nat].

Solution facile : [Y↦Nat, F↦(Nat -> Nat)].

Planche : 20

Pas de solution

À typer : Fun f -> f 1+f.

Equations : [F=Nat -> Y, Y=Nat, F=Nat].

Aucune valeur possible pour F car Nat -> Y ≠ Nat pour tout Y.

C’est donc la résolution qui détecte les errreurs, avec un message du style :

% ocaml
        Objective Caml version 3.10.0

# (fun f -> f 1 + f);;
                  ^
This expression has type int -> int
but is here used with type int

Planche : 21

Pas de solution

À typer : Fun x -> x x.

Équations : [X = X -> Y].

Aucune valeur possible pour X, car les types sont des termes finis.

La résolution detecte un autre style d’erreur, avec :

% ocaml
        Objective Caml version 3.10.0

# (fun x -> x x);;
              ^
This expression has type 'a -> 'b
but is here used with type 'a

Planche : 22

Plusieures solutions

Terme : Fun f -> Fun x -> f x.

Equations : [F= X -> Y].

Une solution φ : [X↦Nat,F↦(Nat -> Nat), Y↦Nat].

Une autre σ : [F↦X -> Y] (il reste des variables !).

Quelle solution ? σ car plus générale (principale).

La solution = une solution principale : φ solution, entraîne il existe ψ avec φ = ψ ∘ σ.

Ici ψ = [X↦Nat, Y↦Nat].

En effet,

ψ(σ(F)) = ψ(X -> Y) = Nat -> Nat

ψ(σ(X)) = ψ(X) = Nat

ψ(σ(Y)) = ψ(Y) = Nat

ψ(σ(Z)) = ψ(Z) = Z

Planche : 23

Plusieures solutions

Terme : Fun b -> Fun x -> Fun y -> Ifz b Then x Else y.

Type : B -> X -> Y -> X.

Equations : [B=Nat, X=Y].

Une solution σ : [B↦Nat, X↦Y].

Une autre solution σ′ : [B↦Nat, Y↦X].

Les deux solutions sont principales :

σ′ = [Y↦X] ∘ σ

σ = [X↦Y] ∘ σ′

Planche : 24

Algorithme de Robinson

Produit une solution principale σ d’un système E.

Informellement : par réécriture de l’ensemble E, jusqu’à ce qu’il soit une substitution (idempotente).

On choisit une équation de E non-encore examinée.

A -> B=C -> D, remplacer par [A=C, B=D].
Nat=Nat ou X=X, supprimer.
Nat=A -> B (ou symétrique), échouer.
X=A (ou symétrique), où X apparaît dans A, échouer.
X=A (ou symétrique) et X n’apparaît pas dans A, remplacer X par A dans les autres équations.

Planche : 25

Terminaison de l’algorithme de Robinson

À l’étape 5. on garde l’équation X=A qui est maintenant examinée. La variable X est résolue, elle n’apparaît plus dans les équations non-examinées.

Soit la paire d’entiers naturels (V(E),|E|).

V(E) nombre de variables non-résolues.
|E| taille des équations.

L’algo termine, car (V(E),|E|) décroit strictement (ordre lexicographique).

Cas 1. et 2.
- V(E) stable (peut décroître si X=X unique équation qui contient X ),
- |E| décroît.
Cas 5. V(E) décroît.

Planche : 26

Correction

L’algorithme produit un système de la forme :

mgu(E) = [X₁=C₁,…,X_m=C_m]

Où les X_i sont deux à deux distincts et n’apparaissent pas dans les C_j. Autrement dit une substitution (idempotente)

[X₁↦C₁,…,X_m↦C_m]

Si mgu(E) n’echoue pas, il produit une solution de E.
Si il existe une solution de E, alors mgu(E) est une solution principale de E.

Planche : 27

Algo de synthèse complet

Synthèse du type de t. En deux étapes :

Calculer ⊢ t ↝ A, E.
Puis, résoudre E, ce qui donne σ

Correction de la synthèse

(Correction) Si pas d’échec ⊢ t:σ(A).
(Complétude) Si ⊢ t:B, alors il existe ψ, tq. B = ψ (σ(A)) (σ(A) type principal).

Planche : 28

Le Fix n’a rien de mystérieux

Fix pow -> Fun n -> Ifz n Then 1 Else 2*pow (n-1)

Soit P type de pow et N type de n.

De (n-1), il vient : [N = Nat] (et aussi [Nat=Nat], mais bon). Type Nat.
De pow (n-1), il vient : [P = (Nat -> Y)]. Type Y.
De 2*pow (n-1), il vient : [Y = Nat]. Type Nat.
De Ifz…, il vient : [N=Nat] (et aussi [Nat=Nat]). Type Nat.
Le type de Fun n -> ⋯ est : N -> Nat.
Le type de Fix pow -> ⋯ est : N -> Nat, avec l’équation : [P =(N -> Nat)].

Planche : 29

Point fixe

Fix pow -> Fun n -> Ifz n Then 1 Else 2*pow (n-1)

Équations,

[N = Nat, P = (Nat -> Y), Y = Nat, N=Nat, P =(N -> Nat)]

Type N -> Nat.

Il n’y a pas « trop » d’équations, chaque équation correspond à une vérification indispensable.

Par ex. la dernière équation contrôle le bon usage de pow relativement à sa définition.

Fix pow -> Fun n -> Ifz n Then 1 Else 2*pow

[N=Nat, P=Nat, P=(N -> Nat)]

Planche : 30

Résolution

[N = Nat, P = (Nat -> Y), Y = Nat, N=Nat, P =(N -> Nat)]

[N↦Nat] et [P = (Nat -> Y), Y = Nat, Nat=Nat, P =(Nat -> Nat)].
[N↦Nat, P↦(Nat -> Y)] et [Y = Nat, Nat=Nat, (Nat -> Y) =(Nat -> Nat)].
[N↦Nat, P↦(Nat -> Nat), Y↦Nat] et [Nat=Nat, (Nat -> Nat) =(Nat -> Nat)]
…
[N↦Nat, P↦(Nat -> Nat), Y↦Nat]

Type du point fixe : N -> Nat soit Nat -> Nat.

Planche : 31

L’unification de ML

Il y a deux différences importantes.

Le polymorphisme.
L’unification est incrémentale (et en place).

Planche : 32

Polymorphisme

Notre système de type ne sait pas typer

Let id = Fun x -> x In
id id

id a le type (principal) X -> X.
Soit l’équation
[(X -> X) = ((X -> X) -> Y)]

Et donc
[X=(X -> X), X=Y]

Qui n’a pas de solution.

Nous verrons cela la semaine prochaine.

Planche : 33

Unification en place

Les types sont en fait un seul graphe que la résolution modifie.

Résoudre :

[…, X=Nat, …]

C’est remplacer X par Nat partout.

Possible en une opération sur un graphe :

⇒

Planche : 34

La résolution immédiate

Au lieu d’accumuler les équations puis de les résoudre.

Les résoudre dès qu’elles sont posées.

Quel intérêt : détection plus précoce de l’échec, et messages d’erreurs en rapport avec le source.

# (fun f -> f 1 + f);;
                  ^
This expression has type int -> int
but is here used with type int

Mais aussi plus proche de l’unification en place pratiquée par ML.

Planche : 35

Une règle de résolution incrémentale

On avait :

E ⊢ t₁ ↝ A₁, E₁ E ⊢ t₂ ↝ A₂, E₂

E ⊢ t₁ t₂ ↝ X, E₁ ⋃ E₂ ⋃ [A₁ = A₂ -> X]

(X frais)

On a :

E, σ ⊢ t₁ ↝ A₁, σ₁ E, σ₁ ⊢ t₂ ↝ A₂, σ₂

E, σ ⊢ t₁ t₂ ↝ X, mgu[A₁ = (A₂ -> X), σ₂]

(X frais)

La forme générale du jugement est

E, σ ⊢ t ↝ A, σ′

Le composant σ représente la solution courante des équations « vues ».

Propriété : σ′ étend σ (σ′ = σ″ ∘ σ) et σ′(E) ⊢ t:σ′(A) (et même type principal).

Planche : 36

L’unification incrémentale

Soit σ la solution d’un problème d’unification. C’est à dire σ = { X₁ ↦ A₁, …, X_n ↦ A_n }, avec :

Les X_i sont deux à deux distincts.
Les X_i n’apparaissent pas dans les A_i.

Et soit une nouvelle équation B = C.

On veut résoudre les équation E = { B = C } ∪ σ.

On pourrait simplement poser mgu(E), mais ça serait dommage d’oublier que σ est déjà résolu.

Planche : 37

Une vue incrémentale de l’unification

Pour résoudre { B = C, X₁ ↦ A₁, …, X_n ↦ A_n }.

Remplacer les X_i par les A_i dans B et C — les X_i n’apparaissent plus.
Résoudre la nouvelle équation : σ′ = { Y₁ ↦ B₁, …, Y_m ↦ B_m} — les X_i n’apparaissent ni dans les Y_j, ni dans les B_j.
Remplacer les Y_i par les B_i dans les A_j, ce qui donne les C_j — les Y_i n’apparaissent plus.
Renvoyer { Y₁ ↦ B₁, …, Y_m ↦ B_m, X₁ ↦ C₁, …, X_n ↦ C_m }.

Cela s’abrège en mgu[σ(B) = σ(C)] ∘ σ.

La notation ∘ exprimant les étapes 3. et 4. mais de façon trop générale (quid si X_i = Y_j ?).

Planche : 38

Toutes les règles

E, σ ⊢ t₁ ↝ A, σ₁ E ⊕ [x = A], σ ⊢ t₂ ↝ B, σ₂

E, σ ⊢ Let x = t₁ In t₂ ↝ B, σ₂

E(x) = A

E, σ ⊢ x ↝ A, σ

E ⊕ [x = X], σ ⊢ t ↝ A, σ′

E, σ ⊢ (Fun x -> t) ↝ X -> A, σ′

(X frais)

E, σ ⊢ t₁ ↝ A, σ₁ E, σ₁ ⊢ t₂ ↝ B, σ₂

E, σ ⊢ t₁ t₂ ↝ X, mgu[σ₂(A) = σ₂(B -> X)] ∘ σ₂

(X frais)

E ⊕ [x = X], σ ⊢ t ↝ A, σ′

E, σ ⊢ (Fix x -> t) ↝ A, mgu[σ′(X) = σ′(A)] ∘ σ′

(X frais)

Planche : 39

Vraiment toutes les règles

E, σ ⊢ n ↝ Nat, σ

E, σ ⊢ t₁ ↝ A₁, σ₁ σ′₁ = mgu[σ₁(A₁) = Nat] ∘ σ₁ E, σ′₁ ⊢ t₂ ↝ A₂, σ₂ σ′₂ = mgu[σ₂(A₂) = Nat] ∘ σ₂

E, σ ⊢ t₁ op t₂ ↝ Nat, σ′₂

E, σ ⊢ t₁ ↝ A₁, σ₁ σ′₁ = mgu[σ₁(A₁) = Nat] ∘ σ₁ E, σ′₁ ⊢ t₂ ↝ A₂, σ₂ E, σ₂ ⊢ t₃ ↝ A₃, σ₃ σ′₃ = mgu[σ₃(A₂) = σ₃(A₃)] ∘ σ₃

E, σ ⊢ Ifz t₁ Then t₂ Else t₃ ↝ A₂, σ′₃

Une fois encore, ces règles expriment une fonction,

E, σ ⊢ t ↝ A, σ′

dont les arguments sont E, σ, t, et dont le résultat est (A,σ′).

Planche : 40

Un exemple

Fix pow -> Fun n -> Ifz n Then 1 Else 2*pow (n-1)

pow est de type P, n est de type N (E est [x:X, pow:P]).

De Ifz, il vient d’abord, σ = [N↦Nat], puis.
- Pour le Then E, σ ⊢ 1 ↝ Nat, σ.
- Et le Else
  - D’abord E, σ ⊢ 2 ↝ Nat, σ,
  - Puis n-1 donne mgu[σ(N)=Nat] ∘ σ qui ne change rien
  - Puis surtout (application pow (n-1)) mgu[σ(P) = σ(Nat -> Y)] ∘ σ. Qui vaut σ′ = [P↦(Nat -> Y),X↦Nat].
  - Et enfin le deuxième argument de « * » conduit au calcul de mgu[σ′(Y) = Nat] ∘ σ′ qui est
    σ″ = [Y↦Nat, P↦(Nat -> Nat), N↦Nat]
Nous avons donc le bilan du typage du Ifz
E, id ⊢ (Ifz n Then 1 Else 2*pow (n-1)) ↝ Nat, σ″
Le type de Fun est N -> Nat,
C’est donc le type de Fix, avec à calculer
mgu[σ″(P) = σ″(N -> Nat)] ∘ σ″

L’équation est triviale, et la substitution ne change pas.

Planche : 41

TP, inférence de type, puis unification.
La prochaine fois, polymorphisme.

Ce document a été traduit de L^AT_EX par H^EV^EA