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

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

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

У меня следующие вопросы:

• Является ли let-полиморфизм характеристикой второго ранга, которая тайно проникла в мир исчисления Милнера первого ранга?

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

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

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

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

• Под эквивалентностью я подразумеваю эквивалентность по модулю аннотаций типов. Подходит ли для этого термин «Система F a la Church»?

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

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