6.4.21. Импредикативный полиморфизм

ImpredicativeTypes

Включает:

RankNTypes

Начиная с:

9.2.1 (ненадёжно в версиях 6.10–9.0)

Разрешает импредикативные полиморфные типы.

Как правило, GHC подставляет в полиморфную функцию только мономорфный тип (то есть тип без forall). Например,

runST :: (forall s. ST s a) -> a
id :: forall b. b -> b

foo = id runST   -- Rejected

Определение foo отклоняется, поскольку пришлось бы подставить в тип id значение b := (forall s. ST s a) -> a, а это запрещено. Подстановка полиморфных типов вместо полиморфных переменных типа называется импредикативным полиморфизмом.

GHC обеспечивает надёжную поддержку импредикативного полиморфизма, включаемую с помощью ImpredicativeTypes и использующую так называемый алгоритм вывода Quick Look. Он описан в статье A quick look at impredicativity (Serrano et al., ICFP 2020).

Включение ImpredicativeTypes

• Включает RankNTypes
• Позволяет указывать в пользовательских типах forall внутри конструкторов типов, а не только внутри стрелок. Например, f :: Maybe (forall a. [a] -> [a]) — допустимая сигнатура типа.
• Разрешает использовать полиморфные типы в видимом применении типов (если включено расширение TypeApplications). Например, можно написать reverse @(forall b. b->b) xs. Видимое применение типов с полиморфным аргументом типа полезно в случаях, когда Quick Look не может вывести правильную подстановку.
• Включает алгоритм вывода типов Quick Look, описанный в статье. Благодаря этому компилятор во многих случаях может выводить импредикативные подстановки для полиморфных функций. Например, reverse xs будет успешно проходить проверку типов даже если xs :: [forall a. a->a], поскольку reverse подставляется типом forall a. a->a.

Обратите внимание: обработка ограничений классов типов и неявных параметров остаётся полностью мономорфной даже при включённом ImpredicativeTypes. В частности:

• Нельзя применять класс типов к полиморфному типу. Следующий пример недопустим: f :: C (forall a. a->a) => [a] -> [a]
• Нельзя объявлять экземпляр с полиморфным аргументом. Следующий пример недопустим: instance C (forall a. a->a)
• Неявный параметр не может иметь полиморфный тип: g :: (?x :: forall a. a->a) => [a] -> [a]

В течение многих лет в GHC существовала особая обработка функции ($), которая позволяет успешно проверять типы выражений вроде runST $ (do { ... }), даже если такая подстановка может быть импредикативной. Эта особая обработка сохранена: даже без ImpredicativeTypes GHC включает Quick Look для применений ($).

Этот флаг был доступен в более ранних версиях GHC (6.10.1–9.0), но его поведение было непредсказуемым и официально не поддерживалось.