Ответ 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".