6.4.19. Полиморфизм произвольного ранга

6.4.19.1. Примеры

Вот примеры объявления data и newtype , конструкторы которых имеют полиморфные аргументы:

data T a = T1 (forall b. b -> b -> b) a

data MonadT m = MkMonad { return :: forall a. a -> m a,
                          bind   :: forall a b. m a -> (a -> m b) -> m b
                        }

newtype Swizzle = MkSwizzle (forall a. Ord a => [a] -> [a])

Конструкторы имеют тип ранга 2:

T1 :: forall a. (forall b. b -> b -> b) -> a -> T a

MkMonad :: forall m. (forall a. a -> m a)
                  -> (forall a b. m a -> (a -> m b) -> m b)
                  -> MonadT m

MkSwizzle :: (forall a. Ord a => [a] -> [a]) -> Swizzle

В более ранних версиях GHC было возможно опустить forall в типе конструктора, если был явный контекст. Например:

newtype Swizzle' = MkSwizzle' (Ord a => [a] -> [a])

С GHC 8.0 объявления, такие как MkSwizzle', вызовут ошибку «вне области действия».

Вы создаете значения типов T1, MonadT, Swizzle, применяя конструктор к подходящим значениям, как обычно. Например,

a1 :: T Int
a1 = T1 (\x y->x) 3

a2, a3 :: Swizzle
a2 = MkSwizzle sort
a3 = MkSwizzle reverse

a4 :: MonadT Maybe
a4 = let r x = Just x
     b m k = case m of
           Just y -> k y
           Nothing -> Nothing
     in
     MkMonad r b

mkTs :: (forall b. b -> b -> b) -> a -> a -> [T a]
mkTs f x y = [T1 f x, T1 f y]

Тип аргумента, как обычно, может быть более общим, чем требуемый тип, как показывает (MkSwizzle reverse). (reverse не требует ограничения Ord).

При использовании сопоставления с образцом связанные переменные теперь могут иметь полиморфные типы. Например:

f :: T a -> a -> (a, Char)
f (T1 w k) x = (w k x, w 'c' 'd')

g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
g (MkSwizzle s) xs f = s (map f (s xs))

h :: MonadT m -> [m a] -> m [a]
h m [] = return m []
h m (x:xs) = bind m x          $ \y ->
             bind m (h m xs)   $ \ys ->
             return m (y:ys)

В функции h мы используем селекторы записей return и bind для извлечения полиморфных функций связывания и возврата из структуры данных MonadT, а не с помощью сопоставления с образцом.

6.4.19.2. Подстановка

Предположим:

f1 :: (forall a b. Int -> a -> b -> b) -> Bool
g1 :: forall x y. Int -> y -> x -> x

f2 :: (forall a. (Eq a, Show a) => a -> a) -> Bool
g2 :: forall x. (Show x, Eq x) => x -> x

тогда f1 g1 и f2 g2 оба правильно типизированы, несмотря на разный порядок переменных типа и ограничений. Что происходит, так это то, что аргумент подставляется, а затем обобщается, чтобы соответствовать типу, ожидаемому функцией.

Но эта подстановка и обобщение происходят только на верхнем уровне типа. В частности, ничего такого не происходит, если `forall` находятся под стрелкой. Например:

f3 :: (Int -> forall a b. a -> b -> b) -> Bool
g3a :: Int -> forall x y. x -> y -> y
g3b :: forall x. Int -> forall y. x -> y -> y
g3c :: Int -> forall x y. y -> x -> x

f4 :: (Int -> forall a. (Eq a, Show a) => a -> a) -> Bool
g4 ::  Int -> forall x. (Show x, Eq x) => x -> x) -> Bool

Тогда применение f3 g3a правильно типизировано, потому что g3a имеет тип, соответствующий типу, ожидаемому f3. Но f3 g3b не правильно типизировано, потому что `forall` находятся в разных местах. Также не правильно типизировано f3 g3c, где `forall` находятся в одном месте, но переменные в другом порядке. Аналогично, f4 g4 не правильно типизировано, потому что ограничения появляются в другом порядке.

Эти примеры можно сделать типизируемыми с помощью расширения eta. Например, f3 (\x -> g3b x) правильно типизирован, аналогично f3 (\x -> g3c x) и f4 (\x -> g4 x).

Похожее явление наблюдается для секций операторов. Например, (\`g3a\` "hello") не правильно типизирован, но его можно сделать типизируемым, расширив его с помощью eta до \x -> x \`g3a\` "hello".

DeepSubsumption

С:

9.2.4

Смягчает простые правила подстановки, неявно вставляя расширения eta при сопоставлении типов функций с различными структурами квантификации.

Расширение DeepSubsumption смягчает упомянутое требование, что `forall` должны появляться в одном месте. GHC вместо этого автоматически перепишет выражения, такие как f x типа ty1 -> ty2 в (\ (y :: ty1) -> f x y); это называется расширением eta. См. раздел 4.6 в Практическое выведение типов для типов произвольного ранга, где этот процесс называется «глубокой схолемизацией».

Обратите внимание, что эти расширения eta могут безмолвно изменить семантику программы пользователя:

h1 :: Int -> forall a. a -> a
h1 = undefined
h2 :: forall b. Int -> b -> b
h2 = h1

С DeepSubsumption, GHC примет эти определения, вставив неявное расширение eta:

h2 = \ i -> h1 i

Это означает, что h2 `seq` () не вызовет ошибку, даже если h1 `seq` () вызовет.

Историческая справка: Глубокая схолемизация первоначально была удалена из языка предложением GHC Proposal #287, но была повторно введена в качестве части расширения DeepSubsumption вслед за GHC Proposal #511.

6.4.19.3. Вывод типов

В общем случае, вывод типов для типов произвольного ранга неразрешим. GHC использует алгоритм, предложенный Одеромски и Лауфером («Применяя аннотации типов», POPL’96), чтобы получить разрешимый алгоритм, потребовав некоторой помощи от программиста. У нас пока нет формального определения «некоторой помощи», но правило таково:

Для переменной, связанной с лямбда-выражением или case-выражением, x, либо программист предоставляет явный полиморфный тип для x, либо GHC предположит, что тип x не содержит квантификаторов для всех типов.

Что значит «предоставить» явный тип для x? Вы можете сделать это, задав сигнатуру типа для x непосредственно, используя сигнатуру типа шаблона (Лексически связанные переменные типов), таким образом:

\ f :: (forall a. a->a) -> (f True, f 'c')

В качестве альтернативы, вы можете задать сигнатуру типа для окружающего контекста, который GHC может «протолкнуть вниз», чтобы найти тип для переменной:

(\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)

Здесь сигнатура типа в выражении может быть протолкнула внутрь, чтобы задать сигнатуру типа для f. Аналогично, и более обычно, можно задать сигнатуру типа для самой функции:

h :: (forall a. a->a) -> (Bool,Char)
h f = (f True, f 'c')

Вам не нужно задавать сигнатуру типа, если переменная, связанная с лямбдой, является аргументом конструктора. Вот пример, который мы видели ранее:

f :: T a -> a -> (a, Char)
f (T1 w k) x = (w k x, w 'c' 'd')

Здесь нам не нужно задавать сигнатуру типа для w, потому что это аргумент конструктора T1, и этого достаточно для GHC.

6.4.19.4. Неявное квантификация

GHC выполняет неявное квантификация следующим образом. На самом внешнем уровне (только) типов, написанных пользователем, если и только если нет явного forall, GHC находит все переменные типов, упомянутые в типе, которые еще не находятся в области видимости, и универсально квантифицирует их. Например, следующие пары эквивалентны:

f :: a -> a
f :: forall a. a -> a

g (x::a) = let
              h :: a -> b -> b
              h x y = y
           in ...
g (x::a) = let
              h :: forall b. a -> b -> b
              h x y = y
           in ...

Обратите внимание, что GHC всегда добавляет неявные квантификаторы на внешнем уровне пользовательского типа; он не ищет самую внутреннюю возможную точку квантификации. Например:

f :: (a -> a) -> Int
         -- MEANS
f :: forall a. (a -> a) -> Int
         -- NOT
f :: (forall a. a -> a) -> Int


g :: (Ord a => a -> a) -> Int
         -- MEANS
g :: forall a. (Ord a => a -> a) -> Int
         -- NOT
g :: (forall a. Ord a => a -> a) -> Int

Если вам нужен последний тип, вы можете написать свои forall явно. Действительно, это настоятельно рекомендуется для типов ранга 2.

Иногда нет «внешнего уровня», в этом случае не происходит никакого неявного квантификации:

data PackMap a b s t = PackMap (Monad f => (a -> f b) -> s -> f t)

Это отклоняется, потому что нет «внешнего уровня» для типов в правой части (было бы ужасно добавлять дополнительные параметры к PackMap), поэтому не происходит никакого неявного квантификации, и объявление отклоняется (с сообщением «f не в области видимости»). Решение: используйте явную forall:

data PackMap a b s t = PackMap (forall f. Monad f => (a -> f b) -> s -> f t)