Почему существуют гибкие и жесткие границы в MLF?

Question

Я работаю над реализацией MLF на основе статьи Повышение ML до силы системы F . В статье типы бумаги определяются как:

t ::= a | g t1 ... tn
o ::= t | ⊥ | ∀(a ≥ o) o | ∀(a = o) o

У меня возникли проблемы с пониманием того, в чем разница между ≥ и = в построении типов? Специально для алгоритма унификации.

Я реализовал алгоритмы унификации и логического вывода в Приложении таким образом, что, похоже, все инварианты этих алгоритмов поддерживаются без какого-либо значимого чтения из связанного вида.

Мне бы хотелось привести пример, когда результат объединения изменяется в зависимости от вида.

Answer 1

Подробно описано в разделе «Наш трек». Я постараюсь дать другое и менее формальное объяснение, которое, надеюсь, поможет вам построить собственную интуицию.

По существу, переменная с жестко связанным типом является MLF-версией слабой переменной ML. Это можно проиллюстрировать на примерах из статьи. С учетом функции

choose x y = if true then x else y

мы можем назначить два различных типа s1 и s2 выражению choose id, которые отличаются только способом количественного определения переменных типа,

 s1 = \forall a. ((a -> a) -> (a -> a))
 s2 = (\forall a. (a -> a)) -> (\forall a. (a -> a))

Очевидно, что ни один тип не является более общим, чем другой в MLF, поэтому мы должны отложить выбор того или иного, введя гибкий тип и присвоив choose id следующий тип

 s3 = (\forall a. a >= (\forall a. a -> a)). (a -> a) 

Мы можем легко увидеть, что и s1, и s2 являются экземплярами s3.

Функция auto (x : \forall a. a -> a) = x x используется как лакмусовая бумажка, показывающая пример функции, которой нельзя присвоить гибкий тип, поскольку ей может быть присвоен тип s2, который хорошо печатает auto succ как (int -> int) -> (int -> int) что, очевидно, приводит к нарушению нашей системы типов (т. е. мы могли бы применить succ succ). Таким образом, нам нужно дать более слабый тип с жесткой границей,

 s4 = (\forall a. a = (\forall a. a -> a)). (a -> a) 

Так что, если ваша реализация позволяет auto succ, то это не звук. Если он не допускает choose id succ или choose id auto, то он является неполным по отношению к бумаге.

P.S. Другие источники интуиции: эта проблема в основном соответствует сдвигу / уменьшению конфликтов при разборе или ленивой / энергичной оценке. Действительно, нам нужно решить, будем ли мы создавать экземпляр приложения типа прямо сейчас или отложить его дальше, и ни один из вариантов не является более общим, чем другой. Поскольку иногда активное создание экземпляров позволяет вводить выражения (например, приписывать s1 к auto), а иногда задерживать нарушения системы типов (приписывая s2 к auto, что позволяет auto succ)