Как Хаскелл добавил Тьюринга-полноту к Системе F?

Я читал разные системы типов и лямбда-исчисления, и я вижу, что все типизированные лямбда-исчисления в лямбда-кубе сильно нормализуют, а не эквивалент Тьюринга. Это включает в себя систему F, просто типизированное лямбда-исчисление плюс полиморфизм.

Это приводит меня к следующим вопросам, для которых я не смог найти приемлемого ответа:

Как формализм (например,) Haskell отличается от исчисления, на котором он якобы основан?
Какие языковые возможности в Haskell не входят в формализм системы F?
Какое минимальное изменение необходимо для полного расчета Turing?

Большое вам спасибо, кто поможет мне понять это.

Ответ 1

Одним словом, общая рекурсия.

Haskell допускает произвольную рекурсию, тогда как система F не имеет формы рекурсии. Отсутствие бесконечных типов означает fix не выражается в виде замкнутого члена.

Нет примитивного понятия имен и рекурсии. Фактически, чистая система F не имеет понятия о таких понятиях, как определения!

Итак, в Haskell это единственное определение - это то, что добавляет завершающую полноту

fix :: (a -> a) -> a
fix f = let x = f x in x

Действительно, эта функция указывает на более общую идею, имея полностью рекурсивные привязки, мы получаем полноту. Обратите внимание, что это относится к типам, а не только к значениям.

data Rec a = Rec {unrec :: Rec a -> a}

y :: (a -> a) -> a
y f = u (Rec u)
  where u x = f $ unrec x x

С бесконечными типами мы можем написать Y combinator (по модулю некоторое разворачивание) и через него общую рекурсию!

В чистой системе F мы часто имеем некоторое неформальное понятие определений, но это просто сокращения, которые должны быть мысленно встроены полностью. Это невозможно в Haskell, так как это создаст бесконечные термины.

Ядро членов Хаскеля без понятия let, where или = сильно нормализуется, так как у нас нет бесконечных типов. Даже это ключевое исчисление терминов не является системой System F. Система F имеет "большую лямбда" или абстракцию типа. Полный член для id в системе F равен

id := /\ A -> \(x : A) -> x

Это потому, что вывод типа для системы F неразрешим! Мы явно обозначаем везде, где и когда мы ожидаем полиморфизма. В Haskell такое свойство будет раздражать, поэтому мы ограничиваем власть Haskell. В частности, мы никогда не выводим полиморфный тип аргумента лямбда Хаскелла без аннотации (могут применяться условия и условия). Вот почему в ML и Haskell

let x = exp in foo

не совпадает с

(\x -> foo) exp

даже если exp не является рекурсивным! Это суть вывода типа HM и алгоритма W, называемого "let generalization".