Позволил ли Милнер полиморфизм рангу 2?

Question

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

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

Мои вопросы:

• Позволяет ли полиморфизм признаку ранга 2, который тайно проник в мир исчисления Милнера 1-го ранга?

• Назначение отдельной конструкции let, по-видимому, указывает, какие типы следует обобщать с помощью средства проверки типов, а какие - нет.Служит ли это для каких-либо других целей?Есть ли какие-либо причины для расширения более мощных систем, например, System F с отдельным let, который не является сахаром?Есть ли какие-либо документы по обоснованию дизайна исчисления Милнера, которые мне больше не кажутся очевидными?

• Существует ли самый общий тип для \a -> (a True, a 1) в Системе F?

• Существуют ли системы типов, закрытые при бета-расширении?Т.е. если P типизируемый и MN = P, то M типизируемый?

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

• Под эквивалентностью я подразумеваю аннотации по модулю типа эквивалентности.Является ли 'System F a la Church' правильным термином для этого?

• Я знаю, что в общем случае основное свойство типизации не имеет места в F, но основной тип может существовать для моегоконкретный термин.

• Под let я имею в виду нерекурсивный аромат let.Расширение системы F с помощью рекурсивного let, очевидно, полезно, поскольку оно допускает отсутствие завершения.

Answer 1

По отношению к четырем задаваемым вопросам:

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

  Обратите внимание, что это значительно проще, чем общий вывод типа ранга 2.

• Обратите внимание, чтоСтрого говоря, let .. = .. in .. является только синтаксическим сахаром в Системе F, если вы требуете, чтобы в определении была аннотация типа: let ..: .. = .. in ...

• Вот два решения для T в (\ a :: T -> (a True, a 1)) в Системе F: для b.(для a. a -> b) -> (b, b) и для c c.(все a b. a -> b) -> (c, d).Обратите внимание, что ни один из них не является более общим, чем другой.В общем, система F не допускает главных типов.

• Полагаю, это верно для лямбда-исчисления с простыми типами?

Answer 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 иметь в себе какой-нибудь нетипичный мертвый код.

Answer 3

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

Answer 4

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

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

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

Answer 5

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

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