Каковы пределы вывода типа?

Question

Каковы пределы вывода типа?В каких системах типов нет общего алгоритма вывода?

Answer 1

Джо Уэллс показали, что вывод типа неразрешим для Системы F, которая представляет собой самое базовое полиморфное лямбда-исчисление, независимо открытое Жираром и Рейнольдсом.Это наиболее важный результат, показывающий пределы вывода типа.

Вот важная проблема, которая все еще остается открытой:как лучше всего интегрировать обобщенные алгебраические типы данных в вывод типов Хиндли-Милнера?Каждый год Саймон Пейтон Джонс придумывает новые ответы, которые предположительно лучше, чем ответ предыдущего года.Я не читал версию за март 2009 года и поэтому не могу сказать, считаю ли я ее окончательной.

Answer 2

Система зависимых от значения типов (или, короче говоря, система зависимых типов) может описывать типы, которые говорят что-то вроде:«Во время оценки (во время выполнения) значение этой переменной всегда будет равно значению этой переменной, которая вычисляется с помощью другого процесса оценки».Автоматический вывод этого типа из кода влечет за собой автоматическое доказательство теорем.Если набор теорем, которые вы можете выразить, ограничен автоматически доказуемыми, это не будет проблемой, но в случае языков с зависимой типизацией это обычно не так.

Таким образом, зависимо типизированные системы не могут иметь общий (и полный) вывод типов.

Я уверен, что кто-то может дать моральный, формальный и полный ответ...