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

6.4.20.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, чтобы извлечь полиморфные функции bind и return из структуры данных MonadT, а не использовать сопоставление с образцом.

6.4.20.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 имеет некорректный тип, поскольку ограничения указаны в другом порядке.

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

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

DeepSubsumption

Начиная с:

9.2.4

Ослабляет простые правила подчинения, неявно вставляя эта-расширения при сопоставлении типов функций с различными структурами квантификации.

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

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

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

При включённом расширении DeepSubsumption GHC примет эти определения, неявно вставив эта-расширение:

h2 = \ i -> h1 i

Это означает, что h2 `seq` () не вызовет аварийного завершения, хотя h1 `seq` () завершится с ошибкой.

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

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

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

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

Что значит «указать» явный тип для 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.20.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)