Quels sont les systèmes de types connus les plus solides pour lesquels l'inférence est décidable?

Il est bien connu que l'inférence de type Hindley-Milner (le -calculus simplement typé avec polymorphisme) a une inférence de type décidable: vous pouvez reconstruire des types de principe pour n'importe quel programme sans aucune annotation.$\lambda$

L'ajout de classes de style Haskell semble préserver cette décidabilité, mais d'autres ajouts rendent l'inférence sans annotations indécidable (familles de types, GADT, types dépendants, types Rank-N, System , etc.)$\omega$

Je me demande: quels sont les systèmes de type connus les plus solides avec une inférence complètement décidable? Cela va se situer quelque part entre Hindley-Milner (complètement décidable) et les types dépendants (complètement indécidables). Y a-t-il des aspects des DT qui peuvent être ajoutés qui préservent la décidabilité de l'inférence? Quelles recherches ont été effectuées pour voir jusqu'où cela peut être poussé?

Je me rends compte qu'il n'y a pas un seul système le plus fort, qu'il existe probablement d'infinies petites modifications incrémentielles qui peuvent être ajoutées à HM en gardant l'inférence. Mais il y a probablement quelques candidats pratiques de systèmes qui ont été découverts.

Edit: étant donné qu'il n'y a pas de système "le plus fort", j'accepterai une réponse qui décrit les systèmes notables qui étendent Hindley Milner avec une inférence décidable. Les exemples peuvent être les types liquides, le rang 2, etc.

[EDIT: Voilà quelques mots sur chacun]

Il existe plusieurs façons d'étendre l'inférence de type HM. Ma réponse est basée sur de nombreuses tentatives, plus ou moins réussies, de mise en œuvre de certaines d'entre elles. Le premier sur lequel je suis tombé est le polymorphisme paramétrique . Les systèmes de types essayant d'étendre HM dans cette direction tendent vers le système F et nécessitent donc des annotations de type. Deux extensions notables dans cette direction que j'ai rencontrées sont:

• HMF, il permet l'inférence de type pour tous les types System-F, ce qui signifie que vous pouvez avoir une quantification universelle "au milieu" d'un type, leur apparence n'est pas implicitement située à la portée la plus élevée comme pour les types polymorphes HM. Le document indique clairement qu'il n'existe aucune règle claire quant au nombre et à l'endroit où les annotations de type peuvent être nécessaires. Les types étant également ceux du système F, les termes n'ont généralement pas de type principal.

• MLF n'est pas seulement une extension de HM, c'est aussi une extension de System F qui retrouve la propriété de type principal de HM en introduisant une sorte de quantification bornée sur les types. Une comparaison a été faite par les auteurs, MLF est strictement plus puissant que HMF et les annotations ne sont nécessaires que pour les paramètres utilisés de manière polymorphe.

Une autre façon d'étendre HM consiste à faire varier le domaine des contraintes.

• HM (X) est Hindley-Milner paramétré sur un domaine de contraintes X. Dans cette approche, l'algorithme HM génère les contraintes qui sont envoyées à un solveur de domaine pour X. Pour le HM habituel, le solveur de domaine est la procédure d'unification et le domaine se compose de l'ensemble des termes construits à partir des types et des variables de type.
  Un autre exemple pour X pourrait être des contraintes exprimées dans le langage de l'arithmétique de Presburger (auquel cas l'inférence / vérification de type est décidable) ou dans le langage de l'arithmétique Peano (plus décidable). X varie selon un éventail de théories, chacune ayant ses propres exigences concernant la quantité et la localisation des annotations de type nécessaires et allant de pas du tout à toutes.

• Les classes de types de Haskell sont également une sorte d'extension du domaine de contraintes en ajoutant des prédicats de type du formulaire MyClass(MyType)(ce qui signifie qu'il existe une instance de MyClass pour le type MyType).
  Les classes de type préservent l'inférence de type parce qu'elles sont fondamentalement un concept (presque) orthogonal qu'elles implémentent le polymorphisme ad hoc .
  Par exemple, prenez un symbole valde type val :: MyClass a => apour lequel vous pouvez avoir des instances MyClass A, MyClass Betc. Lorsque vous faites référence à ce symbole dans votre code, c'est en fait parce que l'inférence de type est déjà effectuée que le compilateur peut inférer quelle instance de la classe utiliser. Cela signifie que le type de valdépend du contexte dans lequel il est utilisé. C'est aussi pourquoi l'exécution d'une seule valinstruction conduit à uneambiguous type error : le compilateur ne peut déduire aucun type basé sur le contexte.

Pour les systèmes de types plus avancés comme les GADT, les familles de types, les types dépendants, le système (F) etc., etc., les types ne sont plus des "types", ils deviennent des objets de calcul complexes. Par exemple, cela signifie que deux types qui ne se ressemblent pas ne sont pas nécessairement différents. L'égalité des types ne devient donc pas triviale (du tout).

Pour vous donner un exemple de la complexité réelle, considérons le type de liste dépendant: NList a noù aest le type d'objets dans la liste et nsa longueur.
La fonction append aurait un type append :: NList a n -> NList a m -> NList a (n + m)et la fonction zip serait zip :: NList a n -> NList b n -> NList (a, b) n.
Imaginez maintenant que nous avons le lambda \a: NList t n, b: NList t m -> zip (append a b) (append b a). Ici, le premier argument de zip est de type NList t (n + m)et le second de type NList t (m + n).
Presque la même chose, mais à moins que le vérificateur de type sache que "+" commute sur des nombres naturels, il doit rejeter la fonction car (n + m) n'est pas littéralement (m + n). Il ne s'agit plus d'inférence de type / vérification de type, il s'agit de prouver un théorème.

Les types liquides semblent faire une inférence de type dépendante. Mais si je comprends bien, ce n'est pas vraiment un type dépendant, plus quelque chose comme les types HM habituels sur lesquels une inférence supplémentaire est faite pour calculer les limites statiques.

J'espère que ça aide.