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

ImpredicativeTypes

Подразумевает:

RankNTypes

С:

9.2.1 (ненадёжно в 6.10 - 9.0)

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

В общем случае, GHC будет инстанциировать полиморфную функцию только для мономорфного типа (то есть без foralls). Например,

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
• Позволяет пользователю создавать типы с foralls под конструкторами типов, а не только под стрелками. Например, f :: Maybe (forall a. [a] -> [a]) — это законная сигнатура типа.
• Разрешает полиморфные типы в видимых применениях типа (когда TypeApplications включено). Например, вы можете написать reverse @(forall b. b->b) xs. Использование VTA с полиморфным аргументом типа полезно в тех случаях, когда 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), но поведение было непредсказуемым и не было официально поддержано.