Являются ли Rank2Types/RankNTypes практическими без переменных типа?

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

Например, мы не можем использовать функцию (.), когда промежуточный тип является политипом. Мы вынуждены повторно внедрять (.) На месте. Это, конечно, тривиально для (.), Но проблема для более существенных тел кода.

Я также считаю, что создание ((f. g) x) не эквивалентно (f (g x)) серьезный удар по ссылочной прозрачности и ее преимуществам.

Мне кажется, что это проблема стоп-шоу, и похоже, что расширения Rank * Types почти непрактичны для широкого использования.

Я что-то упустил? Есть ли план, чтобы типы Rank * лучше взаимодействовали с остальной системой типов?

РЕДАКТИРОВАТЬ: Как вы можете использовать типы (runST.всегда)?

Ответ 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 хочет отойти от непроизводительности. Вся эта выразительная сила стоит дорого, и до сих пор не было найдено ни одного доступного и сопутствующего решения.

Ответ 2

Есть ли план, с помощью которого типы Rank * лучше взаимодействуют с остальной системой типов?

Учитывая, насколько распространена монада ST, по крайней мере типы Rank2 достаточно распространены, чтобы быть доказательством обратного. Тем не менее, вы можете посмотреть серию статей "сексуальные/квадратные типы", поскольку способы получения произвольного ранга полиморфизма лучше других с другими.

FPH: первоклассный полиморфизм для Haskell, Dimitrios Vytiniotis, Stephanie Weirich и Simon Peyton Jones, представленный ICFP 2008.

См. также - XImpredicativeTypes - что интересно, для устаревания!

Ответ 3

О ImpredicativeTypes: на самом деле это не влияет (я уверен) на вопрос о пикерах. Это расширение связано с типами данных. Например, GHC скажет вам, что:

Maybe :: * -> *
(forall a. a -> a) :: *

Однако это своего рода ложь. Это верно в неспокойной системе, и в такой системе вы можете написать:

Maybe (forall a. a -> a) :: *

и он будет работать нормально. Это то, что позволяет ImpredicativeTypes. Без расширения подходящий способ подумать об этом:

Maybe :: *m -> *m
(forall a :: *m. a -> a) :: *p

и, таким образом, при попытке сформировать приложение выше существует несоответствие вида.

GHC довольно противоречива на фронте непротиворечивости. Например, тип для id, указанный выше, будет:

id :: (forall a :: *m. a -> a)

но GHC с радостью примет аннотацию (с включенным RankNTypes, но не с ImpredicativeTypes):

id :: (forall a. a -> a) -> (forall a. a -> a)

хотя forall a. a -> a не является монотипом. Таким образом, это позволит использовать нечеткие экземпляры квантифицированных переменных, которые используются только с (->), если вы комментируете как таковые. Но я не думаю, что это приведет к проблемам runST $ .... Раньше это решалось с помощью специального правила экземпляра (подробности, о которых я никогда не упоминал), но это правило было удалено вскоре после его добавления.