Polymorphisme

Planche : 2

A: Polymorphisme.
B: Inférence des types polymorphes.

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.

Solution

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

Enrichir les types :

Nat ∈ T

X ∈ T

A₁ ∈ T A₂ ∈ T

A₁ -> A₂ ∈ T

A ∈ T

∀ X[A] ∈ T

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

E ⊢ t:∀ X[A]

E ⊢ t:A[X↦B]

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

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])[X↦B] = ∀ X[A]

(∀ X[A])[Y↦B] = ∀ X[A[Y↦B]] avec X ∉F(B) (Gros bug !)

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.

(Z -> Z) -> (Z -> Z) = (X -> X)[X↦(Z -> Z)]
Z -> Z=(X -> X)[X↦Z]

Intérêt du polymorphisme

Définir des fonctions dans une bibliothèque, une fois pour toutes.
Les utiliser avec des types divers.

Exemple : composition de fonctions.

Définir :
let (>>>) f g = fun x -> f (g x)
|comp : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b|
Emploi :
let f =
string_of_int >>> (fun x -> x+2) >>> int_of_string
|f : string -> string|

f "5"
|- : string = "7"|

Structures de données polymorphes

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

Nil ([]), de type (∀'a.)'a list.
Cons (::), de type (∀'a.)'a -> 'a list -> 'a list.

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(x₁,f(x₂,… f(x_n,y₀))).

Ou (plus classique) un tri :

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

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

Les entiers (dits de Church)
Let zero = Fun f -> Fun x -> x
Let un = Fun f -> Fun x -> f x
…
L’entier n est le terme
Fun f ->
Fun x ->

f (f ⋯ (f x))

◥
▼
◤

n applications
Le type des entiers est N=∀ X[(X -> X) -> X -> X].

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

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

Successeur
Let succ = Fun n -> Fun f -> Fun x -> n f (f x)
Type N -> N.
Addition et multiplication.
Let add =
  Fun n1 -> Fun n2 ->
    Fun f -> Fun x -> n1 f (n2 f x)
Let mul =
  Fun n1 -> Fun n2 ->
    Fun f -> Fun x -> n1 (n2 f) x
De types N -> N -> N.

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:N; f:Z -> Z; x:Z] ⊢ n f (f x):Z

[n:N; f: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.

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)² = a² + 2ab + b² et donc

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

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 n² pair, on ne peut pas déduire que tous les carrés sont pairs.

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,

En combinait généralisation (abusive) de X, et instanciation de X en Y, on donne n’importe quel type à x.
Et le tour est joué..

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

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

Le système F

E ⊢ t:∀ X[A]

E ⊢ t:A[X↦B]

E ⊢ t:A X ∉F(E)

E ⊢ t:∀ X[A]

E(x) = A

E ⊢ x:A

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

E ⊢ (t₁ t₂):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.

Règles supplémentaires

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

Let x = t₁ In t₂ se type comme (Fun x -> t₂) t₁.
Le type de tout n est Nat, autrement dit.
E ⊢ n:Nat
Types des opérations, par ex. +, vu comme une fonction (+) de type Nat -> Nat -> Nat.
Alors, t₁ + t₂ se comprend comme (+) t₁ t₂.
Plus sioux ifz de type ∀ X[Nat -> X -> X].
Alors, Ifz t₁ Then t₂ Else t₃ se comprend comme ifz t₁ t₂ t₃
Même le Fix peut se voir ainsi comme une règle dérivée…

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.

Retrouver l’inférence

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

Limiter l’instanciation.
- Le ∀ ne peut se trouver que dans les types de l’environnement E.
- ∀ doit se trouver en tête ∀ X₁.∀ X₂…∀ X_n.A
- Toutes les variables sont instanciées à la fois.
Limiter la généralisation.
- La généralisation est aussi complète que possible.
  Pour généraliser le type A dans l’env. E on applique la fonction de généralisation : gen(A,E)
  gen(A,E) = ∀ X₁⋯X_n[A], où { X₁,…,X_n } = F(A) ∖ F(E) (Fpour variables libres)
- Et ne s’applique qu’aux types des variables liées par Let.

Le typage de ML : (Damas Milner)

Types et schémas

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

Nat

A -> B

Schémas de type (S)

∀ X₁⋯X_n[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].

Damas-Milner : règles

E(x) = ∀ X₁⋯X_n[A]

E ⊢ x:A[X₁↦B₁, … , X_n↦B_n]

E ⊢ t₁:A E ⊕ [x:gen(A,E)] ⊢ t₂:B

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

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

E ⊢ (t₁ t₂):B

E ⊕ [x:∀ ∅[A]] ⊢ t:B

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

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

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.

Une règle de résolution immédiate

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

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.

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

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.

L’algorithme J

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

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

E(x) = ∀ X₁ ⋯ X_n[A]

E, σ ⊢ x ↝ A[X₁↦Y₁,…,X_n↦Y_n], σ

(Y₁,…, Y_n frais)

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)

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

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 ↝ X, id

∅, id ⊢ (Fun x -> x) ↝ X -> X, id

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

id, E ⊢ id ↝ Y -> Y, id id, E ⊢ id ↝ Z -> Z, id

id, E ⊢ (id id) ↝ W, mgu[id(Y -> Y) = id((Z -> Z) -> W)] ∘ id

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

Prenons un autre exemple

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

Le Let est à typer dans l’environnement E = [f = ∀ ∅[F], x=∀ ∅[X]]. On type d’abord f x.
- Le typage des variables produit les types F et X.
- On doit résoudre l’équation F = X -> Y, dont la solution est σ = { F ↦ X -> Y }
- Le type de f x est Y.
Généralisé en ∀ ∅[Y], car σ(E) = [f = ∀ ∅[X -> Y],…]. On type donc y+1 dans E′ = E ⊕ [y=∀ ∅[Y]].
Rappelons que y+1 se type comme (+) y 1 avec le type de (+) Nat -> Nat -> Nat.

La suite

[…, y = ∀ ∅[Y]], σ ⊢ ((+) y) 1 ↝ ?, ? avec σ = { F ↦ X -> Y }.
- Typer (+) appliqué à y produit l’équation Nat -> (Nat -> Nat) = Y -> Z, σ devient
  { Y ↦ Nat, Z ↦ Nat -> Nat, F ↦ X -> Nat }
  
  Le type rendu est Z.
- Typer (+) y appliqué à 1, produit l’équation Nat -> Nat = Nat -> W, σ devient
  { W ↦ Nat, Y ↦ Nat, Z ↦ Nat -> Nat, F ↦ X -> Nat }
  
  Le type rendu est W.
Le type de Let y = f x In y+1 est donc W.
Le type de Fun x -> ⋯ est X -> W, celui de Fun f -> ⋯ est F -> (X -> W), soit finalement (X -> Nat) -> X -> Nat.

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

La surcharge (quel est le type de fun x -> x+x ?).
Le typage de l’égalité (=:'a -> 'a -> bool) n’est pas bien satisfaisant, si 'a vaut 'b -> 'c…
Les systèmes avec sous-typage (inférence difficile).

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.

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<String> p = new Poly<String> () ;
    Poly<String> q = 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

TP, inférence des types polymorphes.
La prochaine fois, PCF avec :=, ! etc.

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

Planche : 1

Planche : 2

Planche : 3

Limitation des types simples

Planche : 4

Solution

Planche : 5

En passant…

Planche : 6

Identitité polymorphe

Planche : 7

Intérêt du polymorphisme

Planche : 8

Structures de données polymorphes

Planche : 9

Intérêt théorique du polymorphisme

Planche : 10

Introduction du ∀

Planche : 11

Introduction du ∀

Planche : 12

Et si on ne fait pas attention

Planche : 13

Le système F

Planche : 14

Règles supplémentaires

Planche : 15

La récursion

Planche : 16

Retrouver l’inférence

Planche : 17

Le typage de ML : (Damas Milner)

Types et schémas

Planche : 18

Damas-Milner : règles

Planche : 19

L’unification incrémentale

Planche : 20

Une règle de résolution immédiate

Planche : 21

L’unification incrémentale

Planche : 22

Une vue incrémentale de l’unification

Planche : 23

Un exemple

Planche : 24

L’algorithme J

Planche : 25

Prenons un exemple

Planche : 26

Prenons un autre exemple

Planche : 27

La suite

Planche : 28

Culture : ML

Planche : 29

Culture : les génériques de Java

Planche : 30