Planche 1
Cours 3
Inférence de type
Polymorphisme
Jean-Jacques.Levy@inria.fr
http://jeanjacqueslevy.net

secrétariat de l'enseignement:
Catherine Bensoussan
cb@lix.polytechnique.fr
Laboratoire d'Informatique de l'X
Aile 00, LIX
tel: 34 67
http://w3.edu.polytechnique.fr/informatique

Planche 2
Références
Planche 3
Plan

  1. Typage à la Church
  2. Inférence de type
  3. Unification
  4. Listes polymorphes
  5. Polymorphisme
Planche 4
Rappel: règles de typage monomorphe
r, x :  t |- x  :  t
r, x :  t |- M  :  t'
r |- l x :  t.M  :  t ® t'
r |- M  :  t ® t'   r |- N  :  t
r |- MN  :  t'
r |-
 
n
 :  int
r |- M  :  int    r |- N  :  int
r |- M Ä N  :  int
r |- M  :  int    r |- N  :  t    r |- N'  :  t
r |- ifz M then N then N'  :  t
r, x :  t |- M  :  t
r |- µ x :  t.M  :  t
r|- M  :  t    r, x :  t |- N  :  t'
r|- let  x  :  t = M in N  :  t'

Planche 5
Présentation de PCF typé à la Church

Termes sans annotations de type. Les règles de typage sont
|- r, x :  t |- x  :  t
r, x :  t |- M  :  t'
r |- l x.M  :  t ® t'
r |- M  :  t ® t'   r |- N  :  t
r |- MN  :  t'
r |-
 
n
 :  int
r |- M  :  int    r |- N  :  int
r |- M Ä N  :  int
r |- M  :  int    r |- N  :  t    r |- N'  :  t
r |- ifz M then N then N'  :  t
r, x :  t |- M  :  t
r |- µ x.M  :  t
r|- M  :  t    r, x :  t |- N  :  t'
r|- let  x = M in N  :  t'

Exercice 1Montrer que le théorème d'unicité n'est plus vrai.

Planche 6
Inférence de type

Ecrire le type de l'argument et des résultats des fonctions peut être pénible. Informatif parfois, mais souvent très redondant.

Par exemple dans
let  f : int®int = l x : int.x in ...
ou même
let  f (x : int):int = x in ...
C'est plus simple d'écrire
let  f = l x.x in ...
ou
let  f(x) = x in ...
et d'avoir le système qui calcule automatiquement le type (s'il existe).

Planche 7
Règles de typage monomorphe -- bis

Dans M, toutes les variables libres ou liées sont distinctes (toujours possible par a-conversion). On associe à chaque variable x une variable de type ax et à chaque sous-terme N de M une variable de type aN.

Pour M, on génère un système d'équations C(M) de la manière suivante.
M C(M)
x { aM = ax }
l x.N { aM = ax®aN } È C(N)
NP { aN = aP®aM } È C(N) È C(P)
 
n
{ aM = int }
NÄ P { aM = int = aN = aP } È C(N) È C(P)
ifz N then P then P' { aM = aP = aP',  aN = int } È C(N) È C(P) È C(P')
µ x.N { aM = aN,  aM = ax } È C(N)
let  x=N in P { aM = aP,  ax = aN } È C(N) È C(P)

Planche 8
Exemple

M = let  x = 3 in x + 1
aM = a2,  ax = a3
a3 = int
a2 = int = a4 = a1
a4 = ax
Solution  aM=a1=a2=a3=a4=int

l x.l y.x
aM = ax®a1
a1 = ay®a2
a2 = ax
Solution  aM=ax®ay®ax

Exercice 2Essayer pour fact, let  f = l x.x in f(f 2) et let  f = l x.x in (f f) 2.

Exercice 3Donner les équations générées pour les listes.

Planche 9
Equations sur l'algèbre des types

Trouver un type polymorphe revient à résoudre le système d'équations précédent.

Théorème 1 |- M :  t ssi C(M) admet une solution.

Ce système admet toujours une solution la plus générale: le type principal de M.

Comment la calculer?

Þ théorie de l'unification (logique, 1960), utilisée dans la démonstration automatique pour la méthode dite de résolution.

L'unification sert à trouver des solutions dans des algèbres libres. Plusieurs algorithmes: Robinson (exponentiel, et très simple), Huet, Martelli, Montanari (quasi linéaire et simple), Patterson (linéaire, mais compliqué).

Dans ce cours, nous ne considérerons l'unification que sur l'ensemble des types.

Planche 10
Substitutions et types

t,t' ::= a variable de type
  | int les entiers naturels N
  | t ® t' les fonctions de T dans T'

Une substitution s est une fonction des variables de type dans les types. On écrira s = [a1 \ t1, a2 \ t2, ··· an \ tn] quand son graphe est fini. On l'étend naturellement comme fonction des types dans les types. On écrit ts pour le terme obtenu en appliquant s à t. De même, pour la composition s ° s' de deux substitutions s et s'.

Posons t £ t' ss'il existe s tel que t' = ts
et s £ s' ss'il existe f tel que s' = s ° f.

Remarque: les types ont une structure de treillis vis à vis de £.

De même, tout système d'équations sur les types admet une solution minimale au sens de £, si une telle solution existe.

Planche 11
Unification



mgu(C) est la plus petite solution du système d'équations C si elle existe. Le résultat est donc echec ou une substitution. (most general unifier)

Algorithme de Robinson
mgu (Ø) = identite
mgu ({a=a} È C) = mgu (C)
mgu ({a=t } È C) = mgu (C[a \ t]) ° [a \ t] si a ÏFV(t)
mgu ({ t=a} È C) = mgu (C[a \ t]) ° [a \ t] si a ÏFV(t)
mgu ({ t1® t2 = t'1 ® t'2 } È C) = mgu ({t1 = t'1,  t2 = t'2 } È C)
sinon    mgu (C) = echec

Exercice 4Montrer que cet algorithme termine toujours (Indication compter le nombre de variables). Quelle est sa complexité?

Planche 12
Type principal

Théorème 2 Le type t trouvé pour M en résolvant C(M) par l'algorithme d'unification est principal, c'est-à-dire que si |- M :  t', alors t £ t'.

Exemples

I = l x.x :  a ® a
K = l x.l y.x :  a ® b ® a
S = l x.l y.l z.xz(yz) :  (a ® b ® g) ® (a ® b) ® a ® g
B = l f.l g.l x.g(f x) :  (a ® b) ® (b ® g) ® a ® g

Planche 13
Polymorphisme

Quelques fonctions générales peuvent être réutilisables.

Par exemple l x :  int.x a le même code que l x :  char.x ou l x :  string.x

De même append x  y concatène deux listes sans se soucier du type de leurs éléments.

En ne précisant pas les types, on peut utiliser les fonctions plusieurs fois

Ecrire une fois, utiliser partout (R.Harper)

Planche 14
Listes polymorphes

Dans l'extension de PCF avec les listes, on a pour tout a

Terme Type
nil list(a)
hd list(a) ® a
tl list(a) ® list(a)
:: a ® list(a) ® list(a)

Ni hd ni tl ni :: ne sont des termes de PCF étendu. Mais hd(M), tl(M), M :: N sont des termes de PCF.


En C ou en Java, on peut faire des listes de caractères ou d'Objects. Mais il faut faire des conversions explicites pour passer du type list(a) à ces listes plus spécifiques. En C, ca ne coûte rien, mais ce n'est pas sûr. En Java, il y a vérification dynamique du type quand on passe du type list(Object) au type plus spécifique list(a).

Planche 15
Types polymorphes

Problème Si on veut utiliser les listes de tout type librement dans PCF, il faut pouvoir parler du type list(a) où a est une variable de type.

Comment avoir des termes de type list(a) sans coercions ni vérifications de type dynamique?

Þ Types polymorphes

let  append = µ f.l x.l y.ifnil x then y else (hd x) :: f (tl x)   y in
let  0 = 1 :: 2 :: 3 :: nil in
let  1 = 4 :: 5 :: nil in
let  2 = 6 :: 7 :: 8 :: nil in
let  '0 = 0 :: 1 :: 2 :: nil in
let  '1 = 2 :: nil in
hd (append 0  1) + hd (hd (append '0  '1))

Planche 16
Credo
Polymorphisme
+
Typage statique
Þ
Généralité + Sureté + Efficacité
Planche 17
Types polymorphes fonctionnels

Les fonctions manipulant des listes sont de type polymorphe.

let  map = µ map.l f.l x.
ifnil x then nil else f(hd x) :: map f (tl x) in
map (l x. x+1) (3 :: 4 :: nil)

Rappel: en abrégé, cette fonction peut aussi s'écrire
letrec  map f  x =
ifnil x then nil else f(hd x) :: map f (tl x) in
map (l x. x+1) (3 :: 4 :: nil)
est de type (a®b)®list(a)®list(b)

Même des fonctions (moins utiles) ne travaillant pas sur des listes peuvent avoir des types polymorphes.
let  I = l x.x in ...
let  K = l x.l y.x in ...
let  S = l x.l y.l z.x z (y z) in ...
let  comp = l f. l g. l x. f (g x) in ...


Quels sont les lois de typage de tels termes?
Planche 18
Règles de typage polymorphe
t £ t
r, x :  t |- x  :  t
instanciation
r, x :  t |- M  :  t'
r |- l x.M  :  t ® t'
r |- M  :  t ® t'   r |- N  :  t
r |- MN  :  t'
r |-
 
n
 :  int
r |- M  :  int    r |- N  :  int
r |- M Ä N  :  int
r |- M  :  int    r |- N  :  t    r |- N'  :  t
r |- ifz M then N then N'  :  t
r, x :  t |- M  :  t
r |- µ x.M  :  t
r|- M  :  t    r, x :  Gen(t,r) |- N  :  t'
r|- let  x = M in N  :  t'
généralisation

Légère variation sur les règles monomorphes.

Planche 19
Types polymorphes
t,t' ::= " a1,a2, ··· an.t (n ³ 0)   schéma de type
t,t' ::= a variable de type
  | int les entiers naturels N
  | t ® t' les fonctions de T dans T'
Variables de type libres
FV(a) = {a} FV(" a1,a2, ··· an.t) = FV(t) - {a1,a2, ··· an }
FV(int) = Ø FV(t® t') = FV(t) È FV(t')
FV(Ø) = Ø FV(r,   x:t) = FV(r) È FV(t)

Généralisation
Gen (t, r) = " a1,a2, ··· an.t    où    {a1,a2, ··· an} = FV(t) - FV(r)
Instanciation
t £ " a1,a2, ··· an.t'
ss'il existe t1,t2,··· tn tels que   t = t' [a1 \ t1, a2 \ t2, ··· an \ tn]
Planche 20
Exemples

let  x = 3 in x + 1
r|-
 
3
 :  int   
r, x :  int |- x  :  int    r, x :  int |-
 
1
 :  int
r, x :  int |- x +
 
1
 :  int
r|- let  x =
 
3
in x +
 
1
 :  int

l x.x
l x.l y.x
x : a |- x : a
|- l x.x  :  a®a
x : a,y : b |- x : b
x : a |- l y.x : a®b
|- l x.l y.x  :  a®b®a

let  f = l x.x in f 2
x : a |- x : a
|- l x.x  :  a®a
  
f :  "a.a®a |- f  :  int®int    f :  "a.a®a |-
 
2
 :  int
f :  "a.a®a |- f 
 
2
 :  int
|- let  f = l x.x in f  
 
2
 :  int
Planche 21


Exercice 5En appliquant les règles précédentes, trouver les types de

let  f = l x.x in f(f 2)
let  f = l x.x in (f f) 2
let  x = 2 in let  y = x + 1 in 2 × x + y
let  f = l x. x× x + 1 in f 4 + f 5
let  f = l x. x× x + 1 in f (f x)
let  fact = µ f. l x . ifz  x then 1 else x × f(x-1) in fact 5

Planche 22
Extension avec les listes

t £ "a.list(a)
r |- nil  :  t
nil
M  :  t    N  :  list(t)
r |- M :: N  :  list(t)
cons
r |- M  :  list(t')    r |- N  :  t    r |- N'  :  t
r |- ifnil M then N then N'  :  t
cond'
r |- M  :  list(t)
r |- hd(M)  :  t
hd
r |- M  :  list(t)
r |- tl(M)  :  list(t)
tl

Et si on veut autoriser hd, tl dans le langage, comme citoyen de 1ère classe, on remplace les 2 dernières règles par

t £ "a.list(a)®a
r |- hd  :  t
hd
t £ "a.list(a)®list(a)
r |- tl  :  t
tl

Planche 23
Exercices avec les listes

l x.hd(x)
list(a) ® a £ "a.list(a) ® a
x  :  list(a) |- hd  :  list(a) ® a
   x  :  list(a) |- x  :  a
x  :  list(a) |- hd(x)  :  a
|- l x.hd(x)  :  list(a) ® a

Exercice 6Typer map.
Planche 24
Quelques théorèmes

Proposition 1 Si r |- M :  t, alors r |- M :  t[a\ t']

Théorème 2 [Type principal] Chaque terme M a un type principal. Tous ses autres types s'obtiennent par substitution.

Théorème 3 let  x=M in N est typé ssi M[x \ N] est typé.

Planche 25
En TD

A la maison et prochaine fois

Planche 26
Interpréteur

Donner la valeur et dessiner son arbre de syntaxe abstraite pour les termes:

let  I = l x.x in let  D = l x.xx in II

let  S = l x.l y.l z.x z(y z)in let  K = l x.l y.x in SKK

let  I = l x.x in (l x.xx)(l x.xI)

let  fact = l x.
let  f = µ f.l x.l r. ifz   x then r else f (x-1) (x*r) in
f   x   1 in
fact   5



This document was translated from LATEX by HEVEA.