Qu'est-ce qui rend la déduction de type pour les types dépendants indécidable?

J'ai vu qu'il était mentionné que les systèmes de types dépendants ne sont pas inférables, mais sont vérifiables. Je me demandais s'il existait une explication simple de la raison pour laquelle il en était ainsi et s'il existait ou non une limite de "dépendance" dans laquelle les types peuvent être indexés par des valeurs, en dessous de laquelle l'inférence de type est possible et au-dessus de laquelle elle n'est pas?

Pour une version assez simple de la théorie des types dépendants, Gilles Dowek a donné la preuve de l’indécidabilité de la typabilité dans un contexte non vide:

Gilles Dowek, L’indécidabilité de la typabilité dans le -calcul$\lambda\Pi$

Ce qui peut être trouvé ici .

$\lambda$

L'idée est de coder un problème de correspondance Post en tant que problème de conversion de type, puis de construire avec soin un terme typable si et seulement si les deux types spécifiques sont convertibles. Ceci utilise la connaissance de la forme des formes normales, qui existent toujours dans ce calcul. L'article est court et bien écrit, je n'entrerai donc pas dans les détails ici.

$\lambda$

JB Wells, la typabilité et la vérification de type dans System F sont équivalentes et indécidables .

Ceci peut être trouvé ici . Tout ce que je sais à ce sujet, c'est que cela réduit le problème de la semi-unification (qui est l'unification modulo de l'instanciation de quantificateurs universels et qui est indécidable) à la vérification du type dans le Système F.

Enfin, il est assez facile de montrer que l’habitation de familles dépendantes est indécidable: il suffit de coder un problème Post dans les indices du constructeur. Voici quelques diapositives de Nicolas Oury qui esquissent l’argumentation.

Quant à savoir s’il existe une "limite", cela dépend en grande partie de ce que vous essayez de faire avec vos types dépendants, et il existe de nombreuses approximations qui essaient d’être soit décidables, ou au moins suffisamment proches pour être utilisables. Cependant, ces questions font toujours partie de la recherche active.

Une avenue possible est le champ "types de raffinement" où le langage d’expression des dépendances de types est restreint afin de permettre une vérification décidable, voir par exemple Types de liquides . Il est rare que l'inférence de type complète soit décidable même dans ces systèmes.