Я видел упомянутое, что системы зависимого типа не являются заразными, но проверяемыми. Мне было интересно, есть ли простое объяснение, почему это так, и есть ли предел «зависимости», где типы могут быть проиндексированы по значениям, ниже какого типа вывод возможен, а выше которого нет?
42
Ответы:
Для довольно простой версии теории зависимых типов Жиль Доуек привел доказательство неразрешимости типизации в непустом контексте:
Жиль Даук, Неразрешимость типизируемости в калькулятореλ Π
Который можно найти здесь .
Идея состоит в том, чтобы закодировать проблему почтовой корреспонденции как проблему преобразования типов, а затем тщательно построить термин, который можно вводить, если два конкретных типа являются конвертируемыми. При этом используются знания о форме нормальных форм, которые всегда существуют в этом исчислении. Статья короткая и хорошо написана, поэтому я не буду вдаваться в подробности.
Дж. Б. Уэллс. Типичность и проверка типов в Системе F эквивалентны и неразрешимы .
Это можно найти здесь . Все, что я знаю об этом, - это то, что он сводит проблему полуунификации (которая является объединением по модулю инстанцирования универсальных квантификаторов и неразрешима) к проверке типов в системе F.
Наконец, довольно легко показать, что заселение зависимых семейств неразрешимо: просто закодируйте проблему Поста в индексы конструктора. Вот несколько слайдов Николаса Ури, которые иллюстрируют аргумент.
Относительно того, существует ли «предел», это во многом зависит от того, что вы пытаетесь сделать со своими зависимыми типами, и существует множество приближений, которые пытаются либо быть разрешимыми, либо, по крайней мере, достаточно близкими, чтобы их можно было использовать. Эти вопросы все еще являются частью активного исследования.
Одним из возможных путей является поле «уточняющих типов», в котором язык выражения зависимостей типов ограничен, чтобы можно было разрешить проверку, см., Например, « Жидкие типы» . Редко, что вывод полного типа можно решить даже в этих системах.
источник