2.4 Polymorphisme
Le système des types simples ne donne pas le vrai polymorphisme malgré
son ensemble de variables de type.
En effet le terme (l f.ff)(l x.x) n'est pas typable car la variable f prend
deux valeurs : a®a et
(a®a)®a®a.
Ce qui est impossible car une variable ne possède qu'un seul type.
Pour cela on étend le système de type.
Soit P un ensemble de variables de types,
T l'ensemble des types simples construit à partir de T et S
l'ensemble des schémas de types construit à partir de P et T.
-
types simples :
-
si aÎ P alors aÎ T
- si s,tÎ T alors s®tÎ T.
- schémas de type :
-
si tÎ T alors tÎ S
- si sÎ S,aÎ P alors "a.sÎ S
On obtient ainsi de nouvelles règles de typage :
(Var)-
(x1:s1),...,(xn:sn)
|- xi:t [ti/ai]
si="a1,...,an.t
- (App)
-
C|- M:t®t
C|- N:t
C|- MN:t
- (Abs)
-
(x:t),C|- M:t
C|-l x.M:t®t
- (Let)
-
C|- N:t a1,...,an=V(t)-V(C) (x:"a1,...,an.t) C|- M:t
C|- let x = N in M:t
Ce qui nous permet de typer let f = l x.x in ff :
VAR f:"b.b®b |- f:(a®a)®a®a VAR f:"b.b®b|- f:a®a
|- l x.x:b®b b=V(b®b)-V(Ø) f:"b.b®b|- ff:a®a |- let f = l x.x in f f:a®a