16. Inférence de type Hindley/Milner▲
Ce chapitre présente les types de données de Scala et la reconnaissance de motif en développant un système d'inférence de type à la Hindler/Milner (8). Le langage source pour l'inférenceur de type est Mini-ML, du lambda-calcul avec une instruction let. Les arbres syntaxiques abstraits pour Mini-ML sont représentés par les types de données suivants :
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
abstract class Term {}
case class Var(x: String) extends Term {
override def toString = x
}
case class Lam(x: String, e: Term) extends Term {
override def toString = "(\\" + x + "." + e + ")"
}
case class App(f: Term, e: Term) extends Term {
override def toString = "(" + f + " " + e + ")"
}
case class Let(x: String, e: Term, f: Term) extends Term {
override def toString = "let " + x + " = " + e + " in " + f
}
Il y a donc quatre constructeurs d'arbres : Var pour les variables, Lam pour les abstractions de fonctions, App pour l'application des fonctions et Let pour les expressions let. Chaque case classe redéfinit la méthode toString de la classe Any de sorte que les termes s'affichent de façon lisible.
Nous définissons ensuite les types qui sont calculés par le système d'inférence :
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
sealed abstract class Type {}
case class Tyvar(a: String) extends Type {
override def toString = a
}
case class Arrow(t1: Type, t2: Type) extends Type {
override def toString = "(" + t1 + "->" + t2 + ")"
}
case class Tycon(k: String, ts: List[Type]) extends Type {
override def toString =
k + (if (ts.isEmpty) "" else ts.mkString("[", ",", "]"))
}
Il y a trois constructeurs de types : Tyvar pour les variables de type, Arrow pour les types des fonctions et Tycon pour les constructeurs de types comme Boolean ou List. Ce dernier prend en paramètre la liste de leurs paramètres de type - elle est vide pour les constantes de type comme Boolean. Les constructeurs de types implémentent également la méthode toString pour que les types s'affichent correctement.
Notez que Type est une classe fermée (sealed), ce qui signifie qu'on ne peut pas l'étendre avec des sous-classes ou des constructeurs de types en dehors de la suite de définitions dans lequel il est défini. Type est donc un type algébrique fermé qui n'a que trois possibilités. Term, au contraire, est un type algébrique ouvert pour lequel on pourra définir d'autres possibilités.
Les parties principales de l'inférenceur de type sont contenues dans l'objet typeInfer. Nous définissons d'abord une fonction utilitaire qui crée de nouvelles variables de type :
2.
3.
4.
object typeInfer {
private var n: Int = 0
def newTyvar(): Type = { n += 1; Tyvar("a" + n)
}
Nous définissons ensuite une classe pour les substitutions. Une substitution est une fonction idempotente des variables de types vers les types. Elle fait correspondre un nombre fini de variables de types à des types et ne modifie pas les autres variables de types. La signification d'une substitution est étendue à une correspondance point à point des types vers les types.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
14.
15.
abstract class Subst extends Function1[Type,Type] {
def lookup(x: Tyvar): Type
def apply(t: Type): Type = t match {
case tv @ Tyvar(a) => val u = lookup(tv); if (t == u) t else apply(u)
case Arrow(t1, t2) => Arrow(apply(t1), apply(t2))
case Tycon(k, ts) => Tycon(k, ts map apply)
}
def extend(x: Tyvar, t: Type) = new Subst {
def lookup(y: Tyvar): Type = if (x == y) t else Subst.this.lookup(y)
}
val emptySubst = new Subst { def lookup(t: Tyvar): Type = t }
}
Les substitutions sont représentées par des fonctions de type Type => Type. Pour ce faire, la classe Subst hérite du type de fonction unaire Function1[Type, Type] (9). Pour être une instance de ce type, une substitution s doit implémenter une méthode apply prenant un Type comme paramètre et renvoyant un autre Type comme résultat. Une application de fonction s(t) est alors interprétée comme s.apply(t).
Dans la classe Subst, la méthode lookup est abstraite. Il existe deux formes concrètes de substitutions qui diffèrent par leur implémentation de cette méthode. La première est définie par la valeur emptySubst, la seconde par la méthode extend de la classe Subst.
Le type suivant définit les schémas de types, qui sont formés d'un type et d'une liste de noms de variables de types qui apparaissent avec des quantificateurs universels dans le schéma. Le schéma kitxmlcodeinlinelatexdvp\forall a \forall b.a \rightarrow bfinkitxmlcodeinlinelatexdvp, par exemple, serait représenté sous la forme suivante dans le vérificateur de type :
TypeScheme(List(Tyvar("a"), Tyvar("b")), Arrow(Tyvar("a"), Tyvar("b")))La définition de classe des schémas de types n'a pas de clause extends, ce qui signifie que ces schémas sont des classes qui héritent directement de AnyRef. Bien qu'il n'y ait qu'un moyen possible de construire un schéma de type, nous avons choisi d'utiliser une case classe, car ceci permet de décomposer simplement une instance en ses différentes parties :
2.
3.
4.
5.
case class TypeScheme(tyvars: List[Tyvar], tpe: Type) {
def newInstance: Type = {
(emptySubst /: tyvars) ((s, tv) => s.extend(tv, newTyvar())) (tpe)
}
}
Les objets schémas de types disposent d'une méthode newInstance qui renvoie le type contenu dans le schéma après que toutes les variables de types quantifiées universellement ont été renommées en nouvelles variables. L'implémentation de cette méthode accumule (avec /:) les variables de types du schéma avec une opération qui étend une substitution s donnée en renommant une variable de type tv donnée en nouvelle variable de type. La substitution ainsi obtenue renomme toutes les variables de types du schéma. Elle est ensuite appliquée à la partie type du schéma.
Le dernier type dont nous avons besoin dans l'inférenceur de type est Env, un type pour les environnements qui associe des noms de variables à des schémas de type. Il est représenté par l'alias de type Env dans le module typeInfer :
type Env = List[(String, TypeScheme)]Il y a deux opérations possibles sur les environnements. La fonction lookup renvoie le schéma de type associé à un nom ou null si le nom n'est pas enregistré dans l'environnement :
2.
3.
4.
def lookup(env: Env, x: String): TypeScheme = env match {
case List() => null
case (y, t) :: env1 => if (x == y) t else lookup(env1, x)
}
La fonction gen transforme un type donné en un schéma de type en quantifiant toutes les variables de types qui sont libres dans le type, mais pas dans l'environnement :
def gen(env: Env, t: Type): TypeScheme =
TypeScheme(tyvars(t) diff tyvars(env), t)L'ensemble des variables de types libres d'un type est simplement l'ensemble de toutes les variables de types qui apparaissent dans ce type. On le représente ici comme une liste de variables de types :
2.
3.
4.
5.
def tyvars(t: Type): List[Tyvar] = t match {
case tv @ Tyvar(a) => List(tv)
case Arrow(t1, t2) => tyvars(t1) union tyvars(t2)
case Tycon(k, ts) => (List[Tyvar]() /: ts) ((tvs, t) => tvs union tyvars(t))
}
La syntaxe tv @ … du premier motif introduit une variable qui est liée au motif qui suit l'arobase. Notez également que le paramètre de type explicite [Tyvar] dans l'expression de la troisième clause est nécessaire pour que l'inférence de type locale puisse fonctionner.
L'ensemble des variables de types libres d'un schéma de type est l'ensemble des variables de types libres de son composant type, exception faite des variables de types quantifiées :
def tyvars(ts: TypeScheme): List[Tyvar] =
tyvars(ts.tpe) diff ts.tyvarsEnfin, l'ensemble des variables de types libres d'un environnement est l'union des variables de types libres de tous les schémas de types qui y sont enregistrés :
def tyvars(env: Env): List[Tyvar] =
(List[Tyvar]() /: env) ((tvs, nt) => tvs union tyvars(nt._2))Avec Hindley/Milner, l'unification est une opération essentielle de la vérification de type. L'unification calcule une substitution pour que deux types donnés soient égaux (cette substitution est appelée unificateur). La fonction mgu calcule l'unificateur le plus général de deux types t et u donnés sous une substitution s existante. Elle renvoie donc la substitution s' la plus générale qui étend s et qui est telle que les types s(t) et s(u) soient égaux :
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
14.
15.
def mgu(t: Type, u: Type, s: Subst): Subst =
(s(t), s(u)) match {
case (Tyvar(a), Tyvar(b)) if (a == b) =>
s
case (Tyvar(a), _) if !(tyvars(u) contains a) =>
s.extend(Tyvar(a), u)
case (_, Tyvar(a)) =>
mgu(u, t, s)
case (Arrow(t1, t2), Arrow(u1, u2)) =>
mgu(t1, u1, mgu(t2, u2, s))
case (Tycon(k1, ts), Tycon(k2, us)) if (k1 == k2) =>
(s /: (ts zip us)) ((s, tu) => mgu(tu._1, tu._2, s))
case _ =>
throw new TypeError("cannot unify " + s(t) + " with " + s(u))
}
La fonction mgu lance une exception TypeError si aucune substitution unificatrice n'existe. Ceci peut arriver lorsque les deux types ont des constructeurs différents ou parce qu'une variable de type est unifiée avec un type qui contient la variable de type elle-même. Ces exceptions sont modélisées ici comme des instances des case classes qui héritent de la classe Exception prédéfinie.
case class TypeError(s: String) extends Exception(s) {}La tâche principale du vérificateur de type est implémentée par la fonction tp qui prend en paramètres un environnement env, un terme e, un prototype t et une substitution existante s, et qui renvoie une substitution s' qui étend s et qui transforme s (env) e : s (t) en jugement de type dérivable selon les règles de dérivation du système de typage Hindley/Milner. Si cette substitution n'existe pas, la fonction déclenche l'exception TypeError :
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
14.
15.
16.
17.
18.
19.
20.
21.
22.
23.
24.
25.
26.
def tp(env: Env, e: Term, t: Type, s: Subst): Subst = {
current = e
e match {
case Var(x) =>
val u = lookup(env, x)
if (u == null) throw new TypeError("undefined: " + x)
else mgu(u.newInstance, t, s)
case Lam(x, e1) =>
val a, b = newTyvar()
val s1 = mgu(t, Arrow(a, b), s)
val env1 = {x, TypeScheme(List(), a)} :: env
tp(env1, e1, b, s1)
case App(e1, e2) =>
val a = newTyvar()
val s1 = tp(env, e1, Arrow(a, t), s)
tp(env, e2, a, s1)
case Let(x, e1, e2) =>
val a = newTyvar()
val s1 = tp(env, e1, a, s)
tp({x, gen(env, s1(a))} :: env, e2, t, s1)
}
}
var current: Term = null
Pour faciliter la détection des erreurs, la fonction tp stocke le sous-terme analysé dans la variable current : si la vérification de type échoue avec une exception TypeError, cette variable contiendra le sous-terme qui a posé problème.
La dernière fonction du module d'inférence de type, typeOf, est une façade simplifiée de tp. Elle calcule le type d'un terme e dans un environnement env. Pour ce faire, elle crée une nouvelle variable a, calcule une substitution de type qui transforme env e : a en jugement de type dérivable et renvoie le résultat de l'application de la substitution à a :
2.
3.
4.
5.
def typeOf(env: Env, e: Term): Type = {
val a = newTyvar()
tp(env, e, a, emptySubst)(a)
}
} // fin de typeInfer
Pour appliquer l'inférenceur de type, il est pratique de disposer d'un environnement prédéfini contenant des liaisons pour les constantes souvent utilisées. Le module predefined définit par conséquent un environnement env qui contient des liaisons pour les types booléens, numériques et listes, ainsi que certaines opérations primitives définies sur ces types. Il définit également un opérateur de point fixe fix permettant de représenter la récursion :
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
14.
15.
16.
17.
18.
19.
20.
21.
object predefined {
val booleanType = Tycon("Boolean", List())
val intType = Tycon("Int", List())
def listType(t: Type) = Tycon("List", List(t))
private def gen(t: Type): typeInfer.TypeScheme = typeInfer.gen(List(), t)
private val a = typeInfer.newTyvar()
val env = List(
{"true", gen(booleanType)},
{"false", gen(booleanType)},
{"if", gen(Arrow(booleanType, Arrow(a, Arrow(a, a))))},
{"zero", gen(intType)},
{"succ", gen(Arrow(intType, intType))},
{"nil", gen(listType(a))},
{"cons", gen(Arrow(a, Arrow(listType(a), listType(a))))},
{"isEmpty", gen(Arrow(listType(a), booleanType))},
{"head", gen(Arrow(listType(a), a))},
{"tail", gen(Arrow(listType(a), listType(a)))},
{"fix", gen(Arrow(Arrow(a, a), a))}
)
}
Voici un exemple d'utilisation de l'inférenceur de type. Définissons une fonction showType qui renvoie le type d'un terme donné, calculé dans l'environnement predefined.env :
2.
3.
4.
5.
6.
7.
8.
9.
object testInfer {
def showType(e: Term): String =
try {
typeInfer.typeOf(predefined.env, e).toString
} catch {
case typeInfer.TypeError(msg) =>
"\n cannot type: " + typeInfer.current +
"\n reason: " + msg
}
L'application
> testInfer.showType(Lam("x", App(App(Var("cons"), Var("x")), Var("nil"))))donnerait donc la réponse suivante :
> (a6->List[a6])Exercice 16-0-1 : Étendez l'inférenceur de type Mini-ML avec une construction letrec permettant de définir des fonctions récursives et dont la syntaxe est :
letrec ident "=" term in termLe typage de letrec est identique à let sauf que l'identificateur ainsi défini est visible dans l'expression. Avec letrec, la fonction length des listes peut être définie de la façon suivante :
2.
3.
4.
5.
letrec length = \xs.
if (isEmpty xs)
zero
(succ (length (tail xs)))
in ...