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

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

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

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

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

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