La théorie de types a été inventée au début du 20eme siècle avec le but d'éliminer les paradoxes qui viennent de l'application d'une fonction à elle-même. Le lambda calcul a été développé (par Church) vers 1930 comme une théorie de fonctions. En 1940, Church ajoutait les types à son lambda calcul. Ces types étaient simples, ce qui veut dire qu'ils n'étaient jamais construits par des lieurs (comme un $\lambda$). Alors, on a des termes comme $\lambda_{x:T}.B$ (qui sont construits par le lieur $\lambda$) mais on n'a pas des lieurs qu'on peut utiliser pour construire un type.
Malgré l'influence qu'a connue le lambda calcul typé de Church, sa limitation
a aboutit a la création de plusieures théories de types dans la deuxième
partie du 20eme siècle. Dans ces calculs, les types sont construits par des
lieurs. Dans la plupart de ces calculs, on trouve deux lieurs : le
$\lambda$ (pour construire des termes) et le $\Pi$ (ou $\forall$, pour
construire des types). Ces deux lieurs nous permettent de distinguer les
fonctions (qu'on construit avec les $\lambda$s) des types (qu'on
construit avec les $\Pi$). En plus, dans ces calculs, on permet bien
la $\beta$-réduction mais pas la $\Pi$-réduction. Autrement dit, dans ces
calculs on a bien la règle :
$(\lambda_{x:A}.B)C \rightarrow B[x:=C]$
Mais pas la règle :
$(\Pi_{x:A}.B)C \rightarrow B[x:=C]$
En particulier, lorsque $b$ a le type $B$, on donne à $(\lambda_{x:A}.b)C$ le
type $B[x:=C]$ à la place de $(\Pi_{x:A}.B)C$.
Il y a quelques extensions puissantes des théorie des types qui donnent le même comportement au $\Pi$ qu'au $\lambda$ (par exemple, en Automath, dans le langage de programmation Henk de Simon Peyton Jones, etc.). Ca nous aboutit à poser la question : pourquoi distinguer entre le $\lambda$ et le $\Pi$ lorsque des systèmes comme Automath nous montrent qu'il est plus avantageux de traiter les types exactement comme les termes?
Dans cet exposé je décris un système ou les deux lieurs sont identifiés et je montre que ce système a toutes les propriétés qu'on désire d'un système de typage sauf pour l'unicité des types. Mais je démontre aussi que cette perte de l'unicité des types n'est pas grave parce qu'il y a un isomorphisme entre le typage avec deux lieurs et le typage avec un seul lieur et en plus, tous les différent types du même terme, suivent le même modèle.