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       {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 :  t1x2 :  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)   
  W(r + {x : a}, M) = (t', f)      (a variable fraiche)
W(r, MN) = (s(a), s ° f' ° f)   
  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)  
  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)   
  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) Vsñ ® á M [x \ V],  sñ
op
á
 
m

Ä
 
n

sñ ® á
 
m Ä n

sñ
cond1
á ifz
 
0

then M else Nsñ ® á Msñ
cond2
á ifz
 
n

then M else Nsñ ® á Nsñ
(n ¹ 0)
µ á µ x.Msñ ® á M [x \ µ x. M],  sñ
b
 
 
á let  x = V in Nsñ ® á N [x \ V],  sñ
alloc á ref Vsñ ® ás + [=V]ñ    (Ïdomain(s))
deref á !,  sñ ® á s(),  sñ
assign á := Vsñ ® á (),  s[\ V]ñ

On passe aux contextes les réductions précédentes. Ainsi
á Msñ ® á 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 á Msñ ® á M',  s'ñ.


Planche 15

Séquence

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

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

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


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

Remarque: on peut dériver
á Msñ ® á Vs'ñ

á M;Nsñ ®* á Ns'ñ

puisque á M;Nsñ = á let  x= M in Nsñ ® á let  x= V in Ns'ñ ® á Ns'ñ 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ñ ®
á Visñ si s() = [|  V1; V2; ... Vn  |] et 0 £ m < n
err sinon
assign
á [
 
m

] ¬ Vsñ ®
á (),  s[[m]\ V]ñ si s() = [|  V1; V2; ... Vn  |] et 0 £ m < n
err sinon
length
á lengthsñ ® á
 
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.