Каковы пределы вывода типа?
Каковы пределы вывода типа? Какие системы типов не имеют общего алгоритма вывода?
2 ответа
Джо Уэллс показал, что вывод типа неразрешим для Системы F, которая является самым основным полиморфным лямбда-исчислением, независимо обнаруженным Жираром и Рейнольдсом. Это самый важный результат, показывающий пределы вывода типов.
Вот еще одна важная проблема, которая остается открытой: как лучше всего интегрировать обобщенные алгебраические типы данных в вывод типа Хиндли-Милнера? Каждый год Саймон Пейтон Джонс предлагает новые ответы, которые, предположительно, лучше, чем ответы предыдущего года. Я не читал мартовскую версию 2009 года и поэтому не могу сказать, верю ли я, что она будет окончательной.
Система зависимого типа значения (или, короче говоря, система зависимого типа) может описывать типы, которые говорят что-то вроде: "Во время оценки (во время выполнения) значение этой переменной всегда будет равно значению этой переменной, которое вычислено с другим процессом оценки ". Автоматическое выведение этого типа из кода влечет за собой автоматическое доказательство теорем. Если набор теорем, которые вы можете выразить, ограничен автоматически доказываемыми, это не будет проблемой, но в случае языков с зависимой типизацией это обычно не так.
Таким образом, системы с зависимой типизацией не могут иметь общего (и полного) вывода типа.
Я уверен, что кто-то может дать моральный формальный и полный ответ...