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 ⊢ t1:Nat         E ⊢ t2:Nat
E ⊢ t1 op t2:Nat
E ⊢ t1:Nat         E ⊢ t2:A         E ⊢ t3:A
E ⊢ Ifz t1 Then t2 Else t3:A
E ⊢ t1:A -> B         E ⊢ t2:A
E ⊢ t1 t2:B
E ⊢ t1:A         E ⊕ [x:A] ⊢ t2:B
E ⊢ Let x = t1 In t2: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 Et:A1 et Et:A2 pour A1A2.

Par ex.

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

Et

[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

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]

Planche : 9


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


Planche : 10


Retour sur la vérification

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

Nat ∈ T
X ∈ T
A1 ∈ T         A2 ∈ T
A1 -> A2 ∈ 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.


Planche : 11


Variables dans les types

Sémantique :

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

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

Rappels/Remarques.


Planche : 12


Un sens pour les variables de type

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



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

Soit σ une substitution, alors Et:A ⇒ σ(E) ⊢ t:σ(A).

(Avec bien entendu σ(E) défini comme associant σ(E(x)) à x.)


Planche : 13


Autre exemple d’inférence

[f:Fx:X] ⊢ f:F           [f:Fx:X] ⊢ x:X
[f:Fx:X] ⊢ f x:Y
          [f:Fx:X] ⊢ x:X
[f:Fx:X] ⊢ f x+x:Nat
[f:F] ⊢ (Fun x -> f x+x):X -> Nat
 ⊢ (Fun f -> Fun x -> f x+x):F -> 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 -> YY = NatX=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 ↝ AE

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

E(X)=A
E ⊢ x ↝ A, ∅
E ⊢ t1 ↝ A1E1         E ⊢ t2 ↝ A2E2
E ⊢ t1 t2 ↝ XE1 ⋃ E2 ⋃ [A1 = A2 -> X]
(X frais)
E ⊕ [x:X] ⊢ t ↝ AE
E ⊢ (Fun x -> t) ↝ X -> AE
(X frais)

Planche : 16


Production des équations II

Les opérations sur les entiers.

E ⊢ n ↝ Nat, ∅
E ⊢ t1 ↝ A1E1         E ⊢ t2 ↝ A2E2
E ⊢ t1 op t2 ↝ NatE1 ⋃ E2 ⋃ [A1=NatA2=Nat]
E ⊢ t1 ↝ A1E1           E ⊢ t2 ↝ A2E2           E ⊢ t3 ↝ A3E3
E ⊢ Ifz t1 Then t2 Else t3 ↝ A2E1 ⋃ E2 ⋃ E3 ⋃ [A1=NatA2=A3]

Planche : 17


Équations III

E ⊕ [x:X] ⊢ t ↝ AE
E ⊢ (Fix x -> t) ↝ AE ⋃ [X=A]
(X frais)
E ⊢ t1 ↝ A1E1          E ⊕ [x:A1] ⊢ t2 ↝ A2E2
E ⊢ (Let x = t1 In t2) ↝ A2E1 ⋃ E2

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


Planche : 18


Exemple

À typer Fun f -> 2+f 1.

Type : F -> Nat.

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

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

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


Planche : 19


Résoudre

Équations du type E = { A1=B1, …, An=Bn }, avec un langage de termes simple (sans variables liées).

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

[X1C1,…,XmCm]

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

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

Solution facile : [YNat, 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 -> YNat 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 φ : [XNat,F↦(Nat -> Nat), YNat].

Une autre σ : [FX -> 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 ψ = [XNat, YNat].

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 σ : [BNat, XY].

Une autre solution σ′ : [BNat, YX].

Les deux solutions sont principales :

σ′ = [YX] ∘ σ
σ = [XY] ∘ σ′

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.

  1. A -> B=C -> D, remplacer par [A=C, B=D].
  2. Nat=Nat ou X=X, supprimer.
  3. Nat=A -> B (ou symétrique), échouer.
  4. X=A (ou symétrique), où X apparaît dans A, échouer.
  5. 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|).

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


Planche : 26


Correction

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

mgu(E) = [X1=C1,…,Xm=Cm]

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

[X1C1,…,XmCm]
  1. Si mgu(E) n’echoue pas, il produit une solution de E.
  2. 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 :





Correction de la synthèse

  1. (Correction) Si pas d’échec ⊢ t:σ(A).
  2. (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.


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=NatP=NatP=(N  -> Nat)]

Planche : 30


Résolution

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

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


Planche : 31


L’unification de ML

Il y a deux différences importantes.


Planche : 32


Polymorphisme

Notre système de type ne sait pas typer

Let id = Fun x -> x In
id
 id

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 ⊢ t1 ↝ A1E1         E ⊢ t2 ↝ A2E2
E ⊢ t1 t2 ↝ XE1 ⋃ E2 ⋃ [A1 = A2 -> X]
(X frais)

On a :

E, σ ⊢ t1 ↝ A1, σ1         E, σ1 ⊢ t2 ↝ A2, σ2
E, σ ⊢ t1 t2 ↝ Xmgu[A1 = (A2 -> X), σ2]
(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 σ = {  X1A1, …, XnAn }, avec :

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, X1A1, …, XnAn }.

  1. Remplacer les Xi par les Ai dans B et C — les Xi n’apparaissent plus.
  2. Résoudre la nouvelle équation : σ′ = { Y1B1, …, YmBm} — les Xi n’apparaissent ni dans les Yj, ni dans les Bj.
  3. Remplacer les Yi par les Bi dans les Aj, ce qui donne les Cj — les Yi n’apparaissent plus.
  4. Renvoyer { Y1B1, …, YmBm, X1C1, …, XnCm }.

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 Xi = Yj ?).


Planche : 38


Toutes les règles

E, σ ⊢ t1 ↝ A, σ1 E ⊕ [x = A], σ ⊢ t2 ↝ B, σ2
E, σ ⊢ Let x = t1 In t2 ↝ B, σ2
E(x) = A
E, σ ⊢ x ↝ A, σ
E ⊕ [x = X], σ ⊢ t ↝ A, σ′
E, σ ⊢ (Fun x -> t) ↝ X -> A, σ′
(X frais)
E, σ ⊢ t1 ↝ A, σ1           E, σ1 ⊢ t2 ↝ B, σ2
E, σ ⊢ t1 t2 ↝ Xmgu2(A) = σ2(B -> X)] ∘ σ2
(X frais)
E ⊕ [x = X], σ ⊢ t ↝ A, σ′
E, σ ⊢ (Fix x -> t) ↝ Amgu[σ′(X) = σ′(A)] ∘ σ′
(X frais)

Planche : 39


Vraiment toutes les règles

E, σ ⊢ n ↝ Nat, σ
E, σ ⊢ t1 ↝ A1, σ1          σ′1 = mgu1(A1) = Nat] ∘ σ1          E, σ′1 ⊢ t2 ↝ A2, σ2          σ′2 = mgu2(A2) = Nat] ∘ σ2
E, σ ⊢ t1 op t2 ↝ Nat, σ′2
E, σ ⊢ t1 ↝ A1, σ1           σ′1 = mgu1(A1) = Nat] ∘ σ1          E, σ′1 ⊢ t2 ↝ A2, σ2           E, σ2 ⊢ t3 ↝ A3, σ3           σ′3 = mgu3(A2) = σ3(A3)] ∘ σ3
E, σ ⊢ Ifz t1 Then t2 Else t3 ↝ A2, σ′3

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]).


Planche : 41



Ce document a été traduit de LATEX par HEVEA