Aujourd'hui les systèmes de type fait l'objet de notre discussion, comme d'habitude.
  Je crois que toi, le lecteur ou la lectrice, n'a aucune nécessité pour être introduit du système HM, aujourd'hui on fait l'objet de notre discussion les Pros et Cons du système HM, et par ailleurs les problèmes on va rencontrer si l'on choisit d'autres systèmes que HM.

Quelle est la caractèristique du système HM?

On dit souvent du système HM, mais qu'est-ce que le système HM? dit simplement, HM est le système utilisé par le langage ML, et généralement on peut appeller aussi le système de OCaml comme le système HM. Caractérisé par l'utilisation, le HM est un système qui n'a pas besoin de tout annotation, et caractérisé par l'implémentation, le HM est un système qui utilise les types principaux, un résolveur global, avec la généralisation automatique sur les let-expressions.
  Bien, donc HM est bon, il est impeccable, donc pourquoi n'utilise-on pas le système HM partout? Parce que pour soutenir les avantages de HM, il faut circonscrire l'expressibilité du système, par exemple, on ne soutient pas le rank-n-polymorphism et le Higher Kinded Polymorphism

Ce sont quoi? le rank-n-polymorphism nous permet de généraliser la fonction d'ordre supérieur, par exemple, on peut écrire

f:\forall \sigma. (\forall \tau. \tau \to \sigma) \to \tt unit

remarquer comment le quantificateur \tau apparaît à la position d'un paramètre, dans un système soutenant le rank-n-polymorphism, les quantificateurs sont permis d'apparaître arbitrairement profond, cependant, c'est célèbre que le rank-n-polymorphism où n\ge 3 est indécidable. C'est-à-dire rank-2-polymorphisme est encore un choix éligible pour la plupart du langage, cependant, HM ne soutient que le rank-1-polymorpshime, c'est-à-dire le polymorphisme parametrique le plus ordinaire, les quantificateurs ne sont permis d'apparaître qu'à la fonction le plus externe (on dit que c'est la forme prenex).
Quant au Higher Kinded Polymorphism, il permet les paramètres typages d'être des types généralisés.

Mais, ce sont très utile dans certaines circonstances, si nous les voulons, il ne faut pas utiliser l'algorithme HM.

Par ailleurs, le système HM adopt un algorithme global, ça nous dit que le système collecte les symboles dans la fonction entière pour construire un ensemble d'équations, et puis il résoud chaque variable typage dans cet ensemble. Ça fait un problème que, l'endroit où on résoud les équation est différent de l'endroit où on collecte les symboles, quand la résolution fait une erreur, elle ne peut pas rapporter la position précise dans le source, on dit que le système HM a un mauvais localité.

Pour résoudre ces problèmes, on a un autre algorithme, l'inférence locale, mais avant d'approfondir sur ce sujet, il faut expliquer qu'est-ce que le mot "locale" signifie ici.

L'inférence locale vs l'inférence globale

Durant l'inférence d'une fonction, il aura des locations où l'information typage est perdu, auquel il faut les inférer, pour l'inférence globale comme HM, une fonction comme ça peut être typé

function func1(a) {
    var s = a;
    return func2(s);
}

function func2(b) {
    return b += 10;
}

d'abord on assigne les types principaux aux variables, supposons que s: S', a: A', et b: B', depuis func2(b) on a B' = int et S' = B', depuis var s = a on a A' = S', en résoulvant cet ensemble d'équation nous donne b: int, s: int et a: int, easy peasy! Mais remarquer qu'on a collecté les équations globalement, i.e., l'information typage coule entre les noeuds fraternels, mais dans une inférence locale, l'information typage ne peut couler qu'entre les noeuds parentals, donc l'exemple ci-dessus ne peut pas typecheck par rapport à une inférence locale, parce que l'information obtenue depuis l'expression func2(b) ne peut pas couler à l'expression var s = a, donc c'est impossible de savoir le type de s en collectant l'information de func2(s).

C'est précisément pourquoi cette forme d'inférence s'appelle l'inférence locale, les Pros, c'est d'être plus simple que l'inférence globale, durant l'implémentation d'un tel algorithme, on peut trouver qu'on n'a pas en effet besoin de collecter les équations, tous les variables et tous les types perdus sont résoulus in situ, pour que l'exemple ci-dessue devienne éligible pour l'inférence locale, il faut annotater le paramètre a et b comme

function func1(a: int) {
    var s = a;
    return func2(s);
}

function func2(b: int) {
    return b += 10;
}

maintenant l'information typage ne coule que depuis les noeuds parentals aux noeuds fraternels, par exemple l'information a: int coule à l'expression var s = a, mais l'information de func(s) ne coule jamais à ni a ni var s = a.

et c'est pourquoi dans un langage comme C# ou Java, tu vois toujours des fonctions annotatées: de tels langages ne permettent pas de la fonction non annotée, ils ne peut pas les typecheck.
si tu as vu l'article par Pierce & Turner, tu vas savoir aussi que dans un tel algorithme on ne résoud les types qu'aux appels de fonction. Ça rend plus simple le processus de l'inférence, en échange d'un coût mineure: il faut annotater les paramètres.

De plus, l'inférence locale nous fournit une belle localité, puisque tous les variables sont résolu in situ, donc on peut rapporter des erruers dès qu'on les rencontre, ça rend plus bienveillant les messages d'erreur.

La bidirectionalité

  À part de la localité, l'inférence locale possède une autre caractéristique, c'est la bidirectionalité, puisque dans l'inférence locale on ne collecte jamais les équations, on les résoud in situ, donc il faut avoir un point auquel on peut créer une équation et la résoudre immediamment, au-dessus j'ai dit que c'est les appels de fonction, et c'est vrai, mais les chercheurs lui a donné un nom plus exotique: l'inférence locale bidirectionnel, c'est parce que si on voit les appels en vue de l'AST, on trouvera que un point auquel il est exactement un appel est répresenté par un noeud dans l'AST, dit FuncCall, et ses arguments sont les noeuds enfants, pour créer une équation à ce point, d'abord on trouve le type des arguments, puis on trouve le type de la fonction, par exemple, dans le code suivant:

function func<A, B, C>(a: A, b: B, c: C) { 
    // ...
}

func(1, "2", '3')

Le type de la fonction est \forall\tt A, B, C. A \to B \to C \to \tt unit ou (en la forme uncurrié) \tt \forall A, B, C. (A, B, C) \to \tt unit, les type des arguments sont int, string, char respectivement, donc on crée trois équations

et on les résoud in situ pour obtenir l'instantiation de ces trois variables typages, depuis l'AST, ces arguments sont les noeuds enfants et l'appel de fonction func(...) est le noeud parental, donc on peut considerer comme si l'on fait concorder l'information typage au-dessous de ce point (i.e. les types des arguments) avec l'information typage au-dessus de ce point (i.e. le type de la fonction, c'est obtenu du environnement, donc on peut considerer qu'il vient d'un endroit plus haut dans l'AST), c'est deux direction des coulées d'information typage, donc on dit que c'est une inférence bidirectionnel.

Quel est le problème quand on étend l'inférence locale aux sous-types?

  HM, c'est pas très difficile à comprendre, l'inférence locale, c'est aussi. Mais notre discussion a été circonscrit dans un fragment système F pur, sans fait aucune référence à l'extension, maintenant on discute sur une extension particulièrement important et intéressant: le sous-typage.

La première modification le sous-typage fait à l'inférence, c'est de transformer les équations en les inégalités, maintenant au lieu de résoudre une équation comme A = int, il faut résoudre une inégalité comme nothing <: A <: any, A peut être tout type qui satisfait cette inégalité, et on vise à minimiser A, i.e., on trouve un type A tel qu'il soit le type minimal satisfaisant tous les inégalités le contenant, en combinant avec le système F, on dit que c'est le système F sub, écrit F_{<:}, ou on dit que c'est la quantification bornée.

Alors c'est tout? Non, le sous-typage fait le deuxième changement de notre système: dans une inférence locale d'un système F sub, pas seulement les coulées d'information typage entre les noeuds fraternels sont interdits, mais également les coulées qui contiennent d'information typage partielle, par exemple

où g:\tt \forall X. (\mathtt{int} \to X) \to X. Parce que information typage est incomplèt quand on typecheck x => x + 1.

Mais pourquoi ne peut-on pas faire ça? Ça nous semble parfaitement légal. La raison fondamentale de ça c'est que si l'on permet de telles coulées d'information, il nous entraînera peut-être aux résultats illégals, Voici la fonction

ou dans un lanage comme scala, on peut même écrire

def map[X, Y](f: X -> Y, list: List[X]): List[Y]

on peut l'appeler comme

val result: List[int] = map(x => x + 1, list)

où list: List[int]. Maintenant, si l'on traite les arguments en isolation, et on regarde seulement à x => x + 1, comment peut-on calculer le type de x? si on prend une façon plus conservative, la résponse ne peut pas devenir plus simple: non, on ne peut pas déduire ce qu'on peut typer x, parce qu'il n'y a pas d'information, si l'on devient plus aggresif, on peut même permettre de résoudre x depuis x + 1 et conclure que x doit être de type int.

Cette façon nous attire, mais ce n'est plus locale: on fait couler le type de x en arrière, de x + 1 à x, où le premier est plus haut dans l'AST et le dernier est plus bas, le coulant d'information typage traverse plus qu'un niveau. Donc pourquoi est-ce qu'on ne peut pas être plus agile et abandonner ce dogme, mélanger l'inference locale et globale? C'est parce que ça rend plus complexe et impuissante l'inférence locale: elle est désignée d'être un système qui est bien plus simple que l'inférence globale comme HM, deuxièmement, même si l'on permet de la rétropropagation (oui ici je ne fais aucune réference au même concept de ML), elle tend encore à avoir des problèmes, la raison c'est d'avoir le sous-types, par exemple, quand on résoud des inégalités de type, on tend à choisir le résolution le plus petite, ou on choisit un type arbitraire, si on a map(x => x + 1, list), et le typecheck est procédé en isolation (ce qui nous dit que le typecheck de x => x + 1 ne considère pas l'argument list), on peut déduire que ⊥ <: X <: int (parce que + accepte deux int et x est l'argument de +) et notre strategie nous donne la borne inférieur X = ⊥ et donc x: ⊥ et enfin ... on a list: List[⊥], ça n'est pas ce qu'on veut!

Donc, peut-on simplement maximiser au lieu de minimiser un variable typage obtenu de la rétropropagation? Oui peut-être, mais le problème fondamental est la complexité de cette conception viole le but initial de l'inférence locale: un système plus simple à implémenenter.

Cas 1e

Ou, on peut même abandonner la rétropropagation, et en revanche retarder le typecheck de x => x + 1, on typecheck l'argument list en premier pour résoudre int <: X <: ⊤, et puis on calcule le type de x => x + 1 avec la connaissance int <: X <: ⊤ a priori, malheureusement ça ne résoud pas le problème: voici encore l'appel:

val result: List[int] = map(x => x + 1, list)

depuis l'annotation de result on peut avoir ⊥ <: Y <: int, et depuis list on a int <: X <: ⊤, maintenant on a deux problèmes: d'abord, on ne peut pas typecheck x + 1 parce que on ne sait que int <: X, et pour que x + 1 soit légal il faut que X <: int. Ensuite, même si l'on ignore ce problème et procède, on a deux inégalités ⊥ <: Y <: int et int <: X <: ⊤, normalement on choisit la résolution la plus petite donc ici on devrait choisir Y = ⊥, mais c'est absurde! Maintenant on a x => x + 1: X -> ⊥.

Cas 2e

Bien, alors quand on fait face à ces cas (les arguments dont le typecheck dépend sur d'autres arguments), on peut délibérément le maximiser au lieu de minimiser, mais c'est pas d'abord aussi, voici le programme

val result = map(x => x + 1, list)

c'est prèsque le même programme sauf que result n'est pas annoté, encore on a int <: X <: ⊤, mais maintenant on ne peut collecter aucune information sur Y, même si l'on considère le type de x + 1 et ajoute l'inégalité int <: Y <: ⊤ depuis ça. Selon notre discussion, il faut minimiser x => x + 1: X -> Y et maximiser result: List[Y], mais puisque Y apparaît co- et contravariantement dans le type de x => x + 1 et result, ça nous dit qu'il faut "minimiser" Y en maximisant Y, ce qui est clarement impossible.

Quel est le problème fondamental ici? Qui a causé ça? On a deux observation.

1. Sur le cas 1e, la raison de minimiser Y nous donne ⊥ devrait être grâce au fait que le constraint, ou l'inégalité de Y est calculé depuis l'annotation de result, au lieu de typecheck l'expression x => x + 1 lui-même, ça nous explique pourquoi faisant couler l'information typage depuis le deuxième argument list au premier argument x => x + 1 ne marchera pas.

2. Surl le cas 2e, c'est parce que le deuxième argument x => x + 1 n'est pas typé sur son paramètre x!. D'abord, puisque x est typé, on ne performe pas l'inférence sur x: int => x + 1, le typecheck procédera et nous donne même ⊥ <: X <: int (puisque X apparaît contravariantement à x), int <: Y <: ⊤[1^], et cette fois x: int => x + 1 peut être typé directement, on minimise son type au lieu de le maximiser (c'est important), donc en minimisant à la fois tous ces inégalités, on a X = int (remarquer que X apparaît contravariantement dans le type de x: int => x + 1, donc minimisant X -> Y revient à maximiser X) et Y = int, bingo.

Si l'on regarde à ce problème plus profondément, comment peut-on éviter ce problème et par ailleurs améliorer notre algorithme? La méthode, c'est implement d'annoter x! Dans les deux observations ci-dessus, annotant x nous permet de calculer le type de x + 1, i.e. une borne inférieure de Y en typecheck x + 1 elle-même, et ça fait disappraître le choix entre maximisation et minimisation. Remarquer que si l'argument de x => x + 1 n'est pas typé, il faut unifier X, ce qui est le type de x, avec int, ce qui est un type depuis un endroit plus haut dans l'AST parce qu'on ne peut pas calculer x: int en typecheck l'expression x => x + 1 elle-même, donc il faut venir d'autres entroits, par exemple en typecheck le deuxième argument, ça a caractérisé ce problème, et dans l'article de Odersky, il exige qu'on peut unifier un variable typage T avec un type concret A si et seulement si A est calculé quelque part plus bas dans l'AST.

Quelle est l'approache d'Odersky

Dans l'algorithme de Pierce & Turner, le typecheck est séparé en deux pieces: le check mode et le synthesize mode, et on a un concept de "type de contexte", c'est le type qui est "expecté" d'une expression, dans le paragraphe ci-dessus on a pointé le problème réel ici, maintenant Odersky a figuré une méthode pour résoudre ce problème, lors de préserver une formulation rigoureuse, il a crée, la Colored Local Type Inference, le raffinement le plus notable de cette inférence est de permettre de faire couler l'information typage partielle, dans ce cadre l'expression

où

devient typable, parce qu'on peut utiliser l'information partielle \tt int \to X. Dans le paragraph ci-dessus on a déjà su que \tt int est obligatoire ici, alors on fait attention à distinguer les types partiels qui peuvent être utilisés et ceux qui ne le peuvent pas. Cet algorithme sépare tous les types en deux catégories, syntesized ou inherited, ceux qui corrèspondent à le synthesize mode et le check mode dans le système de Pierce & Turner, par défaut, il y a deux règles importants:

1. Tous les variables typages sont inherited pendant l'instantiation.
2. On peut instancier un variable typage X avec un type concret A si et seulement si A est synthesized

int -> X est légal parce que dans ce type on va remplacer X, mais X est à la position covariante, donc lors de remplacer X par int, int est calculé en typecheck l'expression x + 1, il est alors synthesized et éligible pour l'instantiation de X. Mais si \tt g: \forall X. (X\to X) \to X, la remplacement ne pourra pas procéder, car il faut remplace le X contravariant avec int, selon le règle du système d'Odersky, le type d'un appel non typé est toujours inherited, donc int ici est aussi un type inherited, par conséquent, l'unification ne marche pas parce qu'on vient d'essayer d'unifier un variable typage T avec un type inherited int.

Un petit détour: La décidablité d'inférence du System F Sub.

  L'inférence du System F n'est pas décidable, tout le monde le sait. Mais au moins son typecheck est décidable. Pour System F Sub, on a même moins d'espoir: pour des certains algorithmes, les subtyping n'est pas décidable, il y a des certains constructions qui va rendre l'algorithme "loop forever". Et plus mauvais: System F Sub peut simuler le Turing Machine (Pour la démonstration, consultez TAPL chapitre 28), et le plus mauvais: si ton langage utilise un système sous-typage nominal, il est undécidable, Le Microsoft a même écrit un article pour ça (et encore une fois les auteurs incluent Benjamin Pierce.). Alors tu peux vois System S Sub n'est pas un système assez bienveillant, mais il est utile, hmmm...
  Dans notre article prochain on verra que le typeclass évite les undécidabilités de System F Sub en ne utilisant pas le sous-typage dans le système.