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

42

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?

Victor
la source
Pas sûr, mais je suppose que vous pourriez utiliser l'inférence pour déterminer si un calcul est arrêté ou non.
Jmite
est-ce lié à la conversion de type dans les langages de programmation? c'est un problème ouvert ici
vzn
Une autre raison est que les types dépendants n'admettent pas les types principaux. Quel est le type de ? λune.une
Jmite

Réponses:

36

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λΠ

Ce qui peut être trouvé ici .

λ

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.

λ

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.

Cody
la source
Lien de types de liquide cassé
michaelsnowden
@michaelsnowden fixé!
Cody