Les types simples pour le l-calcul typé

2.1 Les types simples pour le l-calcul typé

La syntaxe du l-calcul est identique à celle qui a été introduite précédemment.

Soit P un ensemble de variables de types. On définit l'ensemble des types simples bien formés T (construit à partir de T et du constructeur ®) par :

si aÎ P alors aÎ T
si s,tÎ T alors s®tÎ T.

Typer un terme (clos), c'est lui associer un type. Mais on ne peut pas se contenter de ne typer que les termes clos. Il faut donc se référer à un contexte de types (qui associe à chaque variable libre un type). Donc typer un terme (non nécessairement clos) consistera à lui associer un type dans un certain contexte où se trouvent toutes les variables libres du terme. Donnons une définition plus formelle.

Les contextes sont des listes de couples C=(x₁:s₁),...,(x_n:s_n).

On définit inductivement une relation C|- M:t qui signifie ``M est de type t dans le contexte C'' de la façon suivante :

Si C=(x₁:s₁),...,(x_n:s_n), alors C|- x_i:s_i pour tout i=1,...,n (Var).
Si C|- M:s®t et C|- N:s alors C|- MN:t (App).
Et si (x:s)C|- M:t alors C|-l x.M:s®t (Abs).

Ces règles s'écrivent habituellement :

: (Var)
(x₁:s₁),...,(x_n:s_n) |- x_i:s_i
: (Abs)
(x:s),C|- M:tC|-l x.M:s®t

Exemple de typage : on se propose de typer l'entier de Church ``deux''. C'est l fl x.f(f x). On prouve qu'il admet le type (a®a)®a®a au moyens des règles ci-dessus.

1) on a (x:a),(f:a®a)|- x:a
2) et (x:a),(f:a®a)|- f:a®a
3) donc par 1) et 2) (x:a),(f:a®a)|- fx:a
4) par 2) et 3) on a (x:a),(f:a®a)|- f(fx):a
5) puis par la règle d'abstraction, de 4) on déduit (f:a®a)|- l x.f(fx):a®a
6) et de même (f:a®a)|- l f.l x.f(fx):(a®a)®a®a

Ce qui s'écrit plus facilement en utilisant la deuxième forme des règles :

On a donné une méthode de vérification de typage, mais pas de synthèse d'un type.

Pour ce système de types, il existe une méthode de synthèse utilisant l'unification, que nous allons donner. En voici un avant-goût par le raisonnement intuitif suivant :

On suppose que dans ce terme, f a le type s et x a le type t. Comme on a pu former fx il faut que s soit de la forme t®s₁ et alors fx est du type s₁. Comme on a pu former f(fx), il faut que t=s₁. En conclusion, f:t®t et x:t, et le terme a le type (t®t)®t®t pour n'importe quel type t (en particulier, on peut prendre une variable a).