Le typage de CAML III
Fonctions:
function
x
->
corps
Typage dans
Env
Choisir une nouvelle variable de type,
t
, pour désigner le type de
x
.
t
est donc une inconnue.
Typer
corps
dans
ë
(
x
,
t
)
<|
Env
û
. Fait apparaître des contraintes de typage (
t
=
t
1
).
Faire le bilan des contraintes :
contraintes contradictoires : erreur de typage.
variables de type toutes déterminées:
si
x
:
t
1
et si
corps
:
t
2
, alors
function
x
->
corps
:
t
1
®
t
2
certaines variables de type restent indéterminées: polymorphisme (plus tard)
(
Fun
)
ë
(
x
:
t
1
)
<|
Env
û
|-
corps
:
t
2
Env
|-
function
x
->
corps
:
t
1
®
t
2
