Ответ 1
Самое последнее предложение для типов Rank-N - это связанная с Don FFH бумага. По-моему, это тоже самое приятное из кучки. Основная цель всех этих систем - потребовать как можно меньше аннотаций типов. Проблема в том, что при переходе от Hindley/Milner к System F мы теряем основные типы, а вывод типа становится неразрешимым - отсюда необходимость аннотаций типа.
Основная идея работы "boxy types" заключается в том, чтобы максимально распространять аннотации типов. Контроллер типа переключается между типом проверки и типом вывода типа, и, надеюсь, больше не требуется аннотации. Недостатком здесь является то, что требуется аннотация для типа, трудно объяснить, поскольку она зависит от деталей реализации.
Система Remy 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. Первый - это стандартный тип Hindley/Milner и использует предикативную инстанцирование, а второй использует недействующую инстанцирование. Ни один из них не является более общим, чем другой, поэтому вывод типа должен угадать, какого типа пользователь хочет, и это обычно плохая идея.
MLF вместо этого расширяет систему F с ограниченной количественной оценкой. Основной (= самый общий) тип для приведенного выше примера будет:
choose id :: forall (a < forall b. b -> b). a -> a
Вы можете прочитать это как "choose id имеет тип a to a, где a должен быть экземпляром forall 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. Если вам нужен только тип Hindley/Milner, то аннотации не нужны. Если вам нужен тип более высокого ранга, вам нужно указать запрошенный тип, но только при привязке let (или верхнего уровня).
FPH (например, MLF) поддерживает недействующую инстанцирование, поэтому я не думаю, что ваша проблема применима. Поэтому у него не должно быть проблем с типизацией выражения f . g выше. Однако FPH еще не реализована в GHC, и, скорее всего, этого не произойдет. Трудности возникают из-за взаимодействия с принуждением равенства (и, возможно, ограничения типа класса). Я не уверен, что такое последний статус, но я слышал, что SPJ хочет отойти от непроизводительности. Вся эта выразительная сила стоит дорого, и до сих пор не было найдено ни одного доступного и сопутствующего решения.