Как Haskell добавил полноту по Тьюрингу в System F?

Question

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

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

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

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

Answer 1

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

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

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

Так что в Хаскеле это единственное определение - то, что добавляет тьюринговую полноту

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 комбинатор (по модулю некоторого разворачивания) и через него общую рекурсию!

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

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

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

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

let x = exp in foo

не то же самое, что

(\x -> foo) exp

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