Planche : 1


Polymorphisme


Planche : 2


A
Polymorphisme.
B
Inférence des types polymorphes.

Planche : 3


Limitation des types simples

L’identité Fun x -> x a plusieurs types.

Type principal X -> X.

Mais Let id = Fun x -> x In id id n’est pas typable.

[id:X -> X] ⊢ id ↝ X -> X, ∅           [id:X -> X] ⊢ id ↝ X -> X, ∅
[id:X -> X] ⊢ id id ↝ Y, (X -> X) = ((X -> X) -> Y)

Ce qui conduit finalement à l’équation X=X -> X, qui n’a pas de solution.

Et pourtant, puisque id possède tous les types A -> A, les types suivants sont possibles pour la première et la seconde occurrence de id.

(Z -> Z) -> (Z -> Z)
Z -> Z

Et l’application id id a pour type Z -> Z.


Planche : 4


Solution

Autoriser des instances différentes σ(A) d’un même type.

Enrichir les types :

Nat ∈ T
X ∈ T
A1 ∈ T         A2 ∈ T
A1 -> A2 ∈ T
A ∈ T
∀ X[A] ∈ T

Ajouter une règle « d’élimination » de ∀.

E ⊢ t:∀ X[A]
E ⊢ t:A[XB]

On parle aussi d’instanciation (de la variable liée X).

(Il nous faut aussi une règle « d’introduction » de ∀, mais laissons cela de côté pour le moment).


Planche : 5


En passant…

Les types contienent maintenant un lieur (∀), comme les termes (Fun etc.)

Ceci complique la définition de la substitution qui doit éviter les captures des variables libres.

F(X) = { X }
F(Nat) = ∅
F(A -> B) = F(A) ⋃ F(B)
F(∀ X[A]) = F(A) ∖ {  X  }

Et pour la substitution

(∀ X[A])[XB] = ∀ X[A]
(∀ X[A])[YB] = ∀ X[A[YB]]  avec XF(B) (Gros bug !)

Planche : 6


Identitité polymorphe

Dans l’environnement E = id:∀ X[X -> X], on souhaite typer l’application id id.

On y arrive par exemple ainsi.

E ⊢ id:∀ X[X -> X]
E ⊢ id:(Z -> Z) -> (Z -> Z)
         
E ⊢ id:∀ X[X -> X]
E ⊢ id:Z -> Z
E ⊢ (id id):Z -> Z

Les deux occurrences de id donnent lieu à deux instanciations différentes.


Planche : 7


Intérêt du polymorphisme

Exemple : composition de fonctions.


Planche : 8


Structures de données polymorphes

La liste de X est un type noté (∀'a.)'a list en Caml. Défini par deux « constructeurs »

Toutes les fonctions qui ne « regardent pas » directement les éléments (de type 'a) sont polymorphes.

let rec fold_right f y0 xs = match xs with
| [] -> y0
x::xs -> f x (fold_right f y0 xs)
%fold_right : ('a -> 'b -> 'b) -> 'b -> 'a list -> 'b%

Calcule f(x1,f(x2,… f(xn,y0))).

Ou (plus classique) un tri :

%sort : 'a list -> ('a -> 'a -> bool) -> 'a list%

Planche : 9


Intérêt théorique du polymorphisme

Des constructions classiques du λ-calcul (PCF réduit à Fun, application et variables) sont typables.

Par exemple, l’encodage suivant des entiers, montre que nos constantes et opérateurs sur les entiers sont inutiles (dumoins en théorie).

Type des entiers N=∀ X[(X -> X) -> X -> X]

Certaines primitives (toutes ?) sur les entiers sont alors typables:


Planche : 10


Introduction du

Revenons sur le typage de succ

N=∀ X[(X -> X) -> X -> X]
E ⊢ n:N
E ⊢ n:(Z -> Z-> Z -> Z
          E ⊢ f:Z -> Z
E ⊢ (n f):Z -> Z
         
E ⊢ (f x):Z
[n:Nf:Z -> Zx:Z] ⊢ n f (f x):Z
[n:Nf:Z -> Z] ⊢ (Fun x -> n f (f x)):Z -> Z
[n:N] ⊢ (Fun f -> Fun x -> n f (f x)):(Z -> Z) -> Z -> Z

On veut conclure

[n:N] ⊢ (Fun f -> Fun x -> ⋯):∀ Z[(Z -> Z) -> Z -> Z]

Et donc (variable muette), succ de type N -> N.


Planche : 11


Introduction du 

La règle de généralisation.

E ⊢ t:A
E ⊢ t:∀ X[A]
X ∉F(E)

Pour succ la généralisation est légitime, car Z est quelconque.

Pensons à la locution « Soit n un entier quelconque ».

Par exemple, pour a et b quelconques, (a+b)2 = a2 + 2ab + b2 et donc

∀ ab ∈ ℕ2, (a+b)2 = a2 + 2ab + b2

Pour exprimer « X quelconque » : X n’apparaît pas dans E.

En déduction, cela correspond à l’absence d’hypothèses.

Par ex. de n pair alors n2 pair, on ne peut pas déduire que tous les carrés sont pairs.


Planche : 12


Et si on ne fait pas attention

On peut typer Obj.magic : 'a -> 'b.

[x:X] ⊢ x:X
[x:X] ⊢ x:∀ X[X]
[x:X] ⊢ x:Y
 ⊢ (Fun x -> x):X -> Y

En effet,

let magic = Fun x -> x In (magic 1) 2

Se réduit en 1 2, c-à-d une erreur de type à l’exécution.


Planche : 13


Le système F

E ⊢ t:∀ X[A]
E ⊢ t:A[XB]
E ⊢ t:A          X ∉F(E)
E ⊢ t:∀ X[A]
E(x) = A
E ⊢ x:A
E ⊢ t1:A -> B         E ⊢ t2:A
E ⊢ (t1 t2):B
E ⊕ [x:A] ⊢ t:B
E ⊢ (Fun x -> t):A -> B

De Girard (1970, logicien) et Reynols (1975, informaticien).

Notre présentation est emprunté à Wells (1994), qui a prouvé que la synthèse de type est indécidable.


Planche : 14


Règles supplémentaires

Inutiles, si on considère que les constantes c ont des types présents dans l’environnement de départ.


Planche : 15


La récursion

On suppse donné, un combinateur de point fixe fix de type ∀ X[(X -> X) -> X].

Alors Fix f -> t se type comme fix appliqué à (Fun f -> t).

Au lieu d’ajouter une règle du style :

E ⊕ [f:A] ⊢ t:A
E ⊢ (Fix f -> t):A

On se contente des règles du Fun et de l’application.

E ⊢ fix:∀ X[(X -> X-> X]
E ⊢ Fix:(A -> A-> A
         
E ⊕ [f:A] ⊢ t:A
E ⊢ (Fun f -> t):A -> A
E ⊢ fix (Fun f -> t):A

Une telle simplification n’est pas négligeable, quand on code l’inférence.


Planche : 16


Retrouver l’inférence

L’inférence de type du système F n’est pas décidable.


Planche : 17


Le typage de ML : (Damas Milner)

Types et schémas

Types (A, B etc.), comme avant !

Nat
A -> B
X

Schémas de type (S)

∀ X1Xn[A]

Les schémas sont réservés aux environnements de typage

[⋯ ; x:S; ⋯]

Note : un type ordinaire A est représenté par le schéma ∀ ∅[A].


Planche : 18


Damas-Milner : règles

E(x) = ∀ X1Xn[A]
E ⊢ x:A[X1B1, … , XnBn]
E ⊢ t1:A           E ⊕ [x:gen(A,E)] ⊢ t2:B
E ⊢ (Let x = t1 In t2):B
E ⊢ t1:A -> B         E ⊢ t2:A
E ⊢ (t1 t2):B
E ⊕ [x:∀ ∅[A]] ⊢ t:B
E ⊢ (Fun x -> t):A -> B

Et if:∀ X[Nat -> X -> X], fix:∀ X[(X -> X) -> X] etc.


Planche : 19


L’unification incrémentale

Il devient délicat de procéder à l’inférence en deux phases

Car le language des équations devient plus riche que A=B (il doit comprendre des schémas de type).

Mais la résolution immédiate fonctionne.

Revoyons l’idée : résoudre les équations dès qu’elles sont posées.


Planche : 20


Une règle de résolution immédiate

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 : 21


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 : 22


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 : 23


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 : 24


L’algorithme J

E, σ ⊢ t1 ↝ A, σ1          E ⊕ [x = gen1(A),σ1(E))], σ ⊢ t2 ↝ B, σ2
E, σ ⊢ Let x = t1 In t2 ↝ B, σ2
E(x) = ∀ X1 ⋯ Xn[A]
E, σ ⊢ x ↝ A[X1Y1,…,XnYn], σ
(Y1,…, Yn frais)
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)

Et les constantes ifz de type ∀ X[Nat -> X -> X], fix de type ∀ X[(X -> X) -> X] etc.


Planche : 25


Prenons un exemple

Let id = Fun x -> x In id id

Inférons d’abord le type de Fun x -> x. Rien de bien sorcier.

[x:X], id ⊢ x ↝ Xid
∅, id ⊢ (Fun x -> x) ↝ X -> Xid

On a gen(id(X -> X),id(∅)) = ∀ X[X -> X]. L’application id id est à typer dans E = [id:∀ X[X -> X]].

idE ⊢ id ↝ Y -> Yid           idE ⊢ id ↝ Z -> Zid
idE ⊢ (id id) ↝ Wmgu[id(Y -> Y) = id((Z -> Z-> W)] ∘ id

La résolution donne [Y↦(Z -> Z), W↦(Z -> Z)].


Planche : 26


Prenons un autre exemple

Soit à typer Fun f -> Fun x -> Let y = f x In y+1.


Planche : 27


La suite


Planche : 28


Culture : ML

ML est un language fondée sur le typage de Damas-Milner. La synthèse de type (et donc l’existence de typage principaux) est fondamentale.

Cela pose des problèmes et freine un peu les extensions possibles

Il y a encore de la recherche sur ces questions, les type classes de Haskell proposent une solution intéressante aux deux premiers problèmes.


Planche : 29


Culture : les génériques de Java

Le polymorphisme (paramétrique) existe en Java !

class Poly<E> {
  Poly() {}
  E id(E x) { return x ; }

  public static void main(String [] args) {
    int x = new Poly<Integer>().id(10) ;
    String s = new Poly<String>().id(args[0]) ;
    Poly<Stringp = new Poly<String> () ;
    Poly<Stringq = new Poly<Poly<String>> ().id(p) ;
  }
}

Mais c’est un peu plus explicite qu’en ML. (En échange, le sous-typage est possible.)

Se montre suffisant pour les structure de données (Set<E> etc.)


Planche : 30



Ce document a été traduit de LATEX par HEVEA