Самым последним предложением для типов ранга-N является связанная с FP статья Дона.На мой взгляд, это также самая лучшая из всех.Основная цель всех этих систем - требовать как можно меньше аннотаций типов.Проблема заключается в том, что при переходе от Хиндли / Милнера к Системе 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
Вы можете прочитать это как "choose id имеет тип a до a, где a должен быть экземпляромиз forall b. b -> b ".
Интересно, что одно это не более мощное, чем у стандартного Хиндли / Милнера.MLF, следовательно, также допускает жесткое количественное определение.Следующие два типа эквивалентны:
(forall b. b -> b) -> (forall b. b -> b)
forall (a = forall b. b -> b). a -> a
Жесткое количественное определение вводится аннотациями типов, и технические детали действительно довольно сложны.Положительным моментом является то, что MLF требуется очень мало аннотаций типов, и существует простое правило, когда они необходимы.Недостатки:
Типы могут стать труднее для чтения, потому что правая часть '<' может содержать дополнительные вложенные количественные определения. </p>
До недавнего времени не существовало явно выраженного варианта MLF.Это важно для типизированных преобразований компилятора (как это делает GHC).Часть 3 Кандидатская диссертация Бориса Якобовского имеет первую попытку такого варианта.(Части 1 и 2 также интересны; они описывают более интуитивное представление MLF через «Графические типы».)
Возвращаясь к FPH, его основная идея состоит в том, чтобы использовать методы MLF внутри страны., но требовать аннотации типов для привязок let.Если вам нужен только тип Хиндли / Милнера, аннотации не нужны.Если вам нужен тип с более высоким рангом, вам нужно указать запрошенный тип, но только на привязке let (или на верхнем уровне).
FPH (как MLF) поддерживает непредвиденную реализацию, поэтому я не будуне думаю, что ваша проблема применима.Поэтому не должно возникнуть никаких проблем при наборе выражения f . g выше.Однако FPH еще не реализован в GHC и, скорее всего, не будет.Трудности возникают из-за взаимодействия с принуждением к равенству (и, возможно, с ограничениями классов типов).Я не уверен, каков последний статус, но я слышал, что SPJ хочет отойти от непредсказуемости.Вся эта выразительная сила обходится дорого, и до сих пор не было найдено ни одного доступного и всеобъемлющего решения.