Действительно ли Rank2Types/RankNTypes практичны без переменных политипа?

Самым последним предложением для типов Rank-N является связанный документ FPH Дона. На мой взгляд, это также самое красивое из всех. Основная цель всех этих систем - требовать как можно меньше аннотаций типов. Проблема в том, что при переходе от Хиндли / Милнера к Системе F мы теряем основные типы, и вывод типа становится неразрешимым - отсюда и необходимость в аннотациях типов.

Основная идея работы с «квадратными типами» - максимально возможное распространение аннотаций типов. Средство проверки типов переключается между проверкой типов и режимом вывода типов, и, надеюсь, больше никаких аннотаций не требуется. Обратной стороной здесь является то, что трудно объяснить, требуется ли аннотация типа, потому что это зависит от деталей реализации.

Система MLF Реми - пока что самое хорошее предложение; он требует наименьшего количества аннотаций типов и стабилен при многих преобразованиях кода. Проблема в том, что он расширяет систему типов.Следующий стандартный пример иллюстрирует это:

choose :: forall a. a -> a -> a
id :: forall b. b -> b

choose id :: forall c. (c -> c) -> (c -> c)
choose id :: (forall c. c -> c) -> (forall c. c -> c)

Оба вышеупомянутых типа допустимы в Системе F. Первый - это стандартный тип Хиндли / Милнера и использует предикативное создание экземпляров, второй - импредикативное создание экземпляров. Ни один из типов не является более общим, чем другой, поэтому при выводе типов необходимо угадывать, какой тип нужен пользователю, а это обычно плохая идея.

MLF вместо этого расширяет систему F с помощью ограниченной количественной оценки. Основным (= наиболее общим) типом для приведенного выше примера будет:

choose id :: forall (a < forall b. b -> b). a -> a

Вы можете прочитать это как « select id имеет тип от a до a , где a должен быть экземпляром для всех b. B -> b ".

Интересно, что одно это не мощнее стандартного Хиндли / Милнера. Таким образом, MLF также позволяет жесткую количественную оценку. Следующие два типа эквивалентны:

(forall b. b -> b) -> (forall b. b -> b)
forall (a = forall b. b -> b). a -> a

Жесткая количественная оценка вводится с помощью аннотаций типов, и технические детали действительно довольно сложны. Плюс в том, что MLF нужно очень мало аннотаций типов, и есть простое правило, когда они нужны. Недостатки:

• Типы могут стать труднее читать, потому что правая часть '<' может содержать дополнительные вложенные количественные характеристики.

• До недавнего времени не существовало явно типизированного варианта MLF. Это важно для преобразований типизированного компилятора (как это делает GHC). В части 3 кандидатской диссертации Бориса Якобовского есть первая попытка такого варианта. (Части 1 и 2 также интересны; они описывают более интуитивное представление MLF через «Графические типы».)

Возвращаясь к FPH, его основная идея состоит в том, чтобы использовать методы MLF внутри, но требовать аннотации типов в привязках let . Если вам нужен только тип Хиндли / Милнера, то аннотации не требуются. Если вам нужен тип более высокого ранга, вам нужно указать запрошенный тип, но только в привязке let (или верхнего уровня).

FPH (как и MLF) поддерживает непредикативное создание экземпляров, поэтому я не думаю, что ваша проблема применима. Поэтому у него не должно возникнуть проблем с вводом вашего f. g выражение выше. Однако FPH еще не реализован в GHC и, скорее всего, не будет. Сложности возникают из-за взаимодействия с принуждением к равенству (и, возможно, с ограничениями классов типов). Я не уверен, каков последний статус, но я слышал, что SPJ хочет уйти от непредсказуемости. За всю эту выразительную силу приходится платить, и до сих пор не найдено доступного и комплексного решения.