Planche 1
Cours 4
Inférence de type
polymorphe -- Mémoire
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. Inférence de type polymorphe
  2. Algorithme W (Damas, Milner, Tofte)
  3. Références
  4. Tableaux
  5. Typage des références
  6. Analyse statique
Planche 4
Règles de typage polymorphe -- Rappel

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

Le polymorphisme est induit par les déclarations let  x = M in N.
Planche 5
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 6
Substitutions et types

Une substitution s est une fonction des variables de type dans les types. On écrit s = [a1 \ t1, a2 \ t2, ··· an \ tn] quand son graphe est fini, et on pose domain(s) = {a1, a2, ··· an}.

Une substitution est étendue naturellement en fonction des types dans les types. La composition des substitutions s et s' est notée s ° s'.

Posons s £ s' ss'il existe f tel que s' = s ° f. S'il existe, mgu(t=t') est le plus petit s tel que s(t) = s(t').

Enfin, une substitution f s'étend aussi naturellement à tout environnement r comme suit:
f({x1 :  t1,  x2 :  t2,  ... xn :  tn} = {x1 :  f(t1),  x2 :  f(t2),  ... xn :  f(tn)}

Planche 7
Inférence de type en PCF

Damas-Milner-Tofte ont un algorithme W combinant unification et règles de typage

Entrée de l'algorithme W:

Sortie de W:
Planche 8
Algorithme W

Donnés: r et M. Chercher t et f tels que f(r) |- M :  t
W(r + {x : t}, x) = (t, identite)      ( t instance de t par des variables fraiches)
W(r, l x.M) = (f(a) ® t', f)   où
  W(r + {x : a}, M) = (t', f)      (a variable fraiche)
W(r, MN) = (s(a), s ° f' ° f)   où
  W(r, M) = (t, f) W(f(r), N) = (t', f') s = mgu(f'(t) = t' ® a)
  (a variable fraiche)    Retourner échec si s n'existe pas.
W(r, let  x=M in N) = (t', f' ° f)  où
  W(r,M) = (t, f) W(f(r) + {x : Gen(t,f(r))}, N) = (t', f')
W(r,
 
n
) = (int, identite)
W(r, M Ä N) = (int, s' ° f' ° s ° f)   où
  W(r,M) = (t,f) s = mgu(t = int)
  W((s ° f)(r),N) = (t',f') s'= mgu(t' = int)
  Retourner échec si s ou s' n'existe pas.

Exercice 1Donner l'expression de W pour ifz et µ.

Planche 9
Exemples

l x.x+x
W(Ø,l x.x+x) = (int ® int, [a\int])
W({x : a}, x+x) = (int, [a\int])
W({x : a}, x) = (a, identite)
s = mgu(a = int) = [a\int]
W({x : int}, x) = (int, identite)
s' = mgu(int = int) = identite
let  f = l x.x in f 2
W(Ø,let  f = l x.x in f 
 
2
) = (int, [b\int,g\int])
W(Ø, l x.x) = (a ® a, identite)
W({x : a}, x) = (a, identite)
W({f : "a.a®a}, f 
 
2
) = (int, [b\int,g\int])
W({f : "a.a®a}, f) = (b®b, identite)
W({f : "a.a®a},
 
2
) = (int, identite)
s = mgu (b®b = int®g) = [b\int,g\int])

Planche 10


Proposition 1 [correction]
W (r, M) = (t, f) implique f(r) |- M :  t

Proposition 2 [complétude]
f(r) |- M :  t implique W (r, M) = (t', f') pour un t' et f'.

Proposition 3 [type principal]
W (r, M) = (t, f) et f'(r)|- M :  t' impliquent t £ t' et f £ f'.

Corollaire 4 Ø |- M :  t ssi W(Ø, M) = (t', f') et t' £ t.

Exercice 2Typer l x.l y.x, l x.l y.y, l x.l y.xz(yz), l f.l g.l x.f(g x).

Exercice 3Montrer que l x.xx, l x.x(y(x)) ne sont pas typables.

Exercice 4Montrer que let  f=l x.x in (f f)2 est typable, mais que (l f.(f f)2) (l x.x) ne l'est pas.

Exercice 5Typer let  fact = µ f. l x . ifz  x then 1 else x × f(x-1) in fact 5

Exercice 6Etendre l'algorithme W aux listes.

Planche 11
Mémoire
Planche 12
PCF et Références
Termes
M, N, P ::= ... voir cours précédents
  | ref M création
  | !M valeur
  | M := N modification de valeur
  | () valeur vide

Valeurs
V,V' ::=
 
n
constante entière
  | l x.M abstraction
  |   location
  | () valeur vide

Exemples

let  c = ref 0 in let  x = c :=  !c + 1 in  !c
let  c = ref 0 in let  f = (l x. let  y = c :=  !c + 1 in x) in f(4) + f(5) +  !c
let  c = ref 0 in let  f = (l x.let  y =  !c in let  z = c:= x in y) in f(2) + f(3)

Planche 13
Etat mémoire
s ::= [1 = V1, 2 = V2, ..., n = Vn] (i tous distincts)
domain(s) = {1, 2, ... n}
Règles de réductions
b á (l x.M) V,  sñ ® á M [x \ V],  sñ
op
á
 
m
Ä
 
n
,  sñ ® á
 
m Ä n
,  sñ
cond1
á ifz
 
0
then M else N,  sñ ® á M,  sñ
cond2
á ifz
 
n
then M else N,  sñ ® á N,  sñ
(n ¹ 0)
µ á µ x.M,  sñ ® á M [x \ µ x. M],  sñ
b
 
 
á let  x = V in N,  sñ ® á N [x \ V],  sñ
alloc á ref V,  sñ ® á ,  s + [=V]ñ    (Ïdomain(s))
deref á !,  sñ ® á s(),  sñ
assign á := V,  sñ ® á (),  s[\ V]ñ

On passe aux contextes les réductions précédentes. Ainsi
á M,  sñ ® á M',  s'ñ Þ á C[M],  sñ ® á C[M'],  s'ñ

Planche 14
Exemple

á let  c = ref 0 in let  x = c :=  !c + 1 in  !c,   ñ
® á let  c = in let  x = c :=  !c +
 
1
in  !c,  [ =
 
0
]ñ
® á let  x = :=  ! +
 
1
in  !,  [ =
 
0
]ñ
® á let  x = :=
 
0
+
 
1
in  !,  [ =
 
0
]ñ
® á let  x = :=
 
1
in  !,  [ =
 
0
]ñ
® á let  x = () in  !,  [ =
 
1
]ñ
® á !,  [ =
 
1
]ñ
® á
 
1
,  [ =
 
1
]ñ

Exercice 7Donner les règles d'inférence exactes pour dériver la relation á C[M],  sñ ® á C[M'],  s'ñ à partir de á M,  sñ ® á M',  s'ñ.

Planche 15
Séquence

On dérive les instructions classiques de séquence.

M ;  N
º let  x = M in N où xÏFV(M)

while  M  do  N
º µ x.ifz M then () else N; x

for  x=M  to  N  do  P
º let  f =µ f.l x.l y.ifz  x y then P; f(x+1)  y else () in f M N
où m n = {
0 si m £ n
1 si m > n
.

Remarque: on peut dériver
á M,  sñ ® á V,  s'ñ
á M;N,  sñ ®* á N,  s'ñ

puisque á M;N,  sñ = á let  x= M in N,  sñ ® á let  x= V in N,  s'ñ ® á N,  s'ñ comme x ÏFV(N).

Planche 16
Programmation impérative

Dans M;N, le résultat de M est sans intérêt (cf. le codage avec let ). Ce qui importe est de faire M, puis d'évaluer N. Intuitivement, M a un effet par exemple sur la mémoire.

Beaucoup de langages de programmation distinguent les expressions dont seuls comptent les effets, les instructions, des autres expressions. Leur syntaxe définit séparément expressions et instructions. (cf. Algol, Pascal, Java). Par exemple en C ou Java, une expression e devient l'instruction e; en la post-fixant par point-virgule. Ces langages sont souvent appelés langages impératifs.

D'autres langages donnent un résultat à toute expression, même si un type spécial unit ou void est inventé quand on ne s'intéresse pas vraiment au résultat. Ce sont les langages applicatifs. Par exemple Lisp, ML, Haskell.

Remarque: le théorème de Church-Rosser (confluence) disparait avec les références.

Planche 17
Tableaux

Termes
M, N, P ::= ...  
  | [|  M1; M2; ...; Mn  |] création
  | M[N] valeur d'un élément
  | M[N] ¬ P modification de valeur
  | length M taille d'un tableau

Exemples

let  p = l v.l v'.
let  m = ref (0) in
for i=0 to length v - 1 do
m :=  !m + v[i] * v'[i];
!m in
p  [|  1; 2; 3  |]   [|  10; 20; 30  |]

Planche 18
Règles de réductions pour les tableaux

alloct á [|  V1; V2; ... Vn  |],  sñ ® á ,  s + [ =[|  V1; V2; ... Vn  |] ]ñ    (Ïdomain(s))
accès
á [
 
m
],  sñ ®
á Vi,  sñ si s() = [|  V1; V2; ... Vn  |] et 0 £ m < n
err sinon
assign
á [
 
m
] ¬ V,  sñ ®
á (),  s[[m]\ V]ñ si s() = [|  V1; V2; ... Vn  |] et 0 £ m < n
err sinon
length
á length ,  sñ ® á
 
n
,  sñ si s() = [|  V1; V2; ... Vn  |]

Planche 19
Typage polymorphe des références

ref(t) et unit sont deux nouveaux types.

Les règles de typage polymorphe sont étendues en donnant les types suivants aux 4 nouvelles opérations
()  :  unit
ref  :  "a.a®ref(a)
!  :  "a.ref(a)®a
:=  :  "a.ref(a)®a®unit

On peut donc typer
let  r = ref nil in r :=
 
3
:: nil; (hd  !r)  
 
2
r  :  "a.ref(list(a))
r  :  ref(list(int))
r  :  ref(list(int®int))

Pourtant il y a une erreur à l'exécution!
Interaction entre effets mémoire et instanciation.

Planche 20
Typage polymorphe des tableaux

Exercice 8Inventer un système de typage pour les tableaux.

Exercice 9Montrer que le même problème existe avec les tableaux.

Exercice 10Trouver un contrexemple au typage avec les références et sans les listes.

Planche 21
Intérêt des types

Le système de types de PCF avec références ne respecte plus le théorème de progression.

Aussi le cas de l'héritage dans Eiffel, ou des tableaux en Java.

Les deux théorèmes de préservation des types (subject reduction) et de progression sont deux bons thermomètres pour un système de type. Si non respectés, le type d'un terme peut changer après réduction, ou un terme typé peut se bloquer ou provoquer une erreur avant d'obtenir une valeur. Dans un langage typé, les programmes ne finissent pas par segmentation fault.

Remarque: un langage typé n'empêche pas de faire des vérifications de bornes dans l'accès aux éléments d'un tableau ou des tests de division par zéro (exceptions ¹ erreurs).

Planche 22
Analyse statique de programmes

Statiquement, c'est à dire avant d'exécuter un programme, on peut essayer de déterminer si l'accès aux tableaux ne fera pas de débordements.

Exemples:

let  x = [|  4; 5; 6  |] in x[2]
let  x = 2 in [|  4; 5; 6  |]   [x]
let  s = l v.
let  m = ref (0) in
for i=0 to length v - 1 do
m :=   !m + v[i];
!m in
s  [|  1; 2; 3  |]

Il faut faire une analyse statique d'intervalles. Cela peut être compliqué. Inéquations linéaires (cf. Cousot-Halbwachs, Bourdoncle, Deutsch). En tout état de cause, une telle analyse est impossible dans un langage non typé.

Le typage est une première forme d'analyse statique.
Planche 23
En TD A la maison et prochaine fois

This document was translated from LATEX by HEVEA.