Nous présentons un nouvel algorithme pour un langage de programmation de la famille ML, avec variant polymorphe (type somme), enregistrement (type produit) et sous typage. Ce langage ne nécessite aucune définition de type préalable à l'utilisation d'un constructeur ou d'un enregistrement. Il n'y a a donc pas vraiment de type dans le langage, et notre algorithme répond soit
On peut ensuite réintroduire une notion de type (ce qui est souhaitable bien sur), mais ceux-ci sont en fait des abbréviations pour des fonctions identités partielles définies uniquement sur le type que l'on considère. Par exemple, le type des entiers unaires s'écrit
type nat = Zero[] | Succ[nat]
mais définit en fait la fonction
val rec nat n = match n with Zero[] -> Zero[] | Succ[n'] -> Succ[nat n']
Une indication de type (e : nat) signifie simplement
(nat e). Si notre algorithme répond OK, cela garantit
bien que e est un entier, sinon ou pourrait tomber sur un
cas d'évaluation problématique ce qui n'est pas possible.