Милнер допускает полиморфизм в ранге 2?

let a = b in c можно рассматривать как синтаксический сахар для (\a -> c) b, но в типизированной настройке вообще это не так. Например, в исчислении Милнера let a = \x -> x in (a True, a 1) является типичным, но, по-видимому, эквивалентным (\a -> (a True, a 1)) (\x -> x) не является.

Однако последний является типичным в System F с типом ранга 2 для первой лямбда.

Мои вопросы:

Является ли полиморфизм признаком 2-го уровня, который тайно прокрался в мир ранга 1 другого уровня Милнера?
Цель создания отдельной конструкции let, по-видимому, указывает, какие типы должны быть обобщены с помощью проверки типа, а какие нет. Выполняет ли это какие-либо другие цели? Существуют ли какие-либо причины для расширения более мощных систем, например. Система F с отдельной let, которая не является сахаром? Существуют ли какие-либо документы по обоснованию конструкции исчисления Милнера, которые мне кажутся не очевидными?
Существует ли наиболее общий тип для \a -> (a True, a 1) в System F?
Существуют ли системы типов, закрытые при бета-расширении? То есть если P является типичным и M N = P, то M является типичным?

Некоторые пояснения:

Под эквивалентностью я подразумеваю аннотации эквивалентности по модулю. Является ли "система F a la Church" правильным термином для этого?
Я знаю, что в общем случае основное свойство typing не выполняется в F, но для моего конкретного члена может существовать главный тип.
Под let я имею в виду нерекурсивный вкус let. Расширение системы F с рекурсивным let, очевидно, полезно, поскольку оно допускает прерывание.

Ответ 1

W.r.t. на четыре вопроса:

Ключевое понимание этого вопроса заключается в том, что вместо того, лямбда-абстракции с потенциально полиморфным типом аргументов, мы набирают (сахаризованную) абстракцию, которая (1) применяется ровно один раз и, более того, это (2) применяется к статически известному аргументу. То есть мы можем сначала подвергнуть "аргумент" (т.е. Определения локальное определение), чтобы набрать реконструкцию, чтобы найти ее (полиморфного) типа; затем назначьте найденный тип "параметру", (определение); а затем, наконец, введите тело в расширенном типа.

Обратите внимание, что это значительно легче, чем обычный тип ранга-2 умозаключение.
Заметим, что, строго говоря, пусть.. =.. in.. является синтаксическим сахаром в System F, если вы требуете, чтобы definiendum содержал аннотацию типа: let..:.. =.. in.
Вот два решения для T в (\ a:: T → (a True, a 1)) в системе F: forall b. (forall a. a → b) → (b, b) и forall c d. (for a a. a → b) → (c, d). Обратите внимание, что ни один из них не является более общим, чем другой. В общем случае система F не допускает основных типов.
Я полагаю, что это справедливо для просто типизированного лямбда-исчисления?

Ответ 2

Типы не сохраняются при бета-расширении в любом исчислении, которое может выражать понятие "мертвого кода". Вероятно, вы можете выяснить, как написать что-то подобное этому на любом пригодном для использования языке:

if True then something typable else utter nonsense

Например, пусть M = (\x y -> x) (something typable) и N = (utter nonsense) и P = (something typable), так что M N = P и P являются типичными, но M N не является.

... перечитывая ваш вопрос, я вижу, что вы только требуете, чтобы M был типичным, но мне кажется очень странным, что мне нужно "сохранить под бета-расширением". В любом случае, я не понимаю, почему некоторые аргументы, подобные приведенному выше, не могут применяться: просто пусть M имеет в нем какой-то нетипичный мертвый код.

Ответ 3

Вы можете набрать (\a -> (a True, a 1)) (\x -> x), если вместо обобщения только выражения, вы обобщили все лямбда-абстракции. Сделав это, нужно также создать схемы типов в каждой точке использования, а не просто в той точке, где фактически используется связующее, которое ссылается на них. Я не думаю, что есть какие-то проблемы с этим, за исключением того факта, что он намного менее эффективен. Я вспоминаю некоторое обсуждение этого в TAPL, фактически, делая похожие точки.

Ответ 4

Я вспоминаю много лет назад, видя в книге о лямбда-исчислении (возможно, Барендрегте) систему типов, сохраненную бета-расширением. У нее не было количественной оценки, но она имела дизъюнкцию, чтобы выразить, что термин должен быть одновременно более одного типа, а также омега особого типа, в котором каждый термин обитал. Насколько я помню, последний избегает возражений Дэниэла Вагнера. Хотя каждое выражение было хорошо типизировано, ограничение положения омеги в типе позволило вам определить, какие выражения (слабые?) Гладят нормальные формы.

Также, если я правильно помню, полностью нормальные формы выражений имели основные типы, которые не содержали омега.

Например, главный тип \fx → f (fx) (церковная цифра 2) будет чем-то вроде ((A → B)/\ (B → C)) → A → C

Ответ 5

Невозможно ответить на все ваши очень специализированные вопросы, но нет, это не показатель 2. Когда вы пишете, это просто позволяет количественно определить определения, которые дают полностью полиморфный тип ранга-1, если определение не зависит от некоторого мономорфного значения в пределах области видимости.

Также обратите внимание, что Haskell let известен как let rec на других языках и позволяет определять взаимно-рекурсивные функции и значения. Это то, что вы бы не хотели кодировать вручную с помощью лямбда-выражений и Y-комбинаторов.