6.4.17. Абстракции типов

6.4.17.1. Абстракции типов в шаблонах

Since: GHC 9.2

Синтаксис абстракции типов может использоваться в шаблонах, которые соответствуют конструктору данных. Синтаксис не может использоваться с шаблонами записей или инфиксными шаблонами. Это особенно полезно для связывания экзистенциальных переменных типа, связанных с конструктором данных GADT, как показано в следующем примере:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
import Data.Proxy

data Foo where
  Foo :: forall a. (Show a, Num a) => Foo

test :: Foo -> String
test x = case x of
  Foo @t -> show @t 0

main :: IO ()
main = print $ test (Foo @Float)

В этом примере случай в test связывает экзистенциальную переменную, введённую Foo, которую иначе нельзя было бы назвать и использовать.

Можно связать переменные с любой частью аргументов типа конструктору; нет необходимости, чтобы они были экзистенциальными. Кроме того, можно «сопоставить» часть аргумента типа с использованием конструкторов типа.

Для несколько искусственного примера:

foo :: (Num a) => Maybe [a] -> String
foo (Nothing @[t]) = show (0 :: t)
foo (Just @[t] xs) = show (sum xs :: t)

Здесь мы связываем переменную типа t с типом элементов типа списка, который сам является аргументом Maybe.

Порядок аргументов типа, указанный типами применения в шаблоне, такой же, как и для выражения: либо порядок, заданный пользователем в явном forall в определении конструктора данных, либо, если это не указано, порядок, в котором переменные типа появляются в его сигнатуре слева направо.

Например, если у нас есть следующее объявление в синтаксисе GADT:

data Foo :: * -> * where
  A :: forall s t. [(t,s)] -> Foo (t,s)
  B :: (t,s) -> Foo (t,s)

Тогда аргументы типа для A будут соответствовать сначала s, а затем t, в то время как аргументы типа для B будут соответствовать сначала t, а затем s.

Аргументы типа, появляющиеся в шаблонах, могут влиять на выведенный тип определения:

foo (Nothing @Int) = 0
foo (Just x) = x

будет иметь выведенный тип:

foo :: Maybe Int -> Int

который более ограничен, чем тот, который был бы без применения:

foo :: Num a => Maybe a -> a

Для получения дополнительной информации и деталей относительно применений типа в шаблонах, см. статью Переменные типа в шаблонах Эйнсберга, Брейтнера и Пейтона Джонса. По сравнению с этой статьей, реализация в GHC на данный момент, по крайней мере, вводит одно дополнительное консервативное ограничение, что переменные типа, встречающиеся в шаблонах, не должны уже находиться в области видимости, и поэтому всегда являются новыми переменными, которые связывают только соответствующий тип, а не ссылаются на переменную из внешней области видимости. Дикие карты типа _ могут использоваться в любом месте, где не нужно связывать новые переменные.

6.4.17.2. Абстракции типов в функциях

Since: GHC 9.10

Синтаксис абстракции типов может использоваться в лямбда-выражениях и левых частях функций для ввода в область видимости переменных типа, связанных с невидимыми forall. Например:

id :: forall a. a -> a
id @t x = x :: t

Здесь переменные типа t и a обозначают один и тот же тип, т. е. первый и единственный аргумент типа id. В вызове id @Int у нас есть a = Int, t = Int. Разница в том, что a находится в области видимости в сигнатуре типа, а t находится в области видимости в уравнении функции.

Область видимости a может быть расширена, чтобы охватить уравнение функции, включив ScopedTypeVariables. Использование отдельного связывающего элемента, такого как @t , является современным и более гибким вариантом, способным обрабатывать сценарии более высокого ранга (см. пример higherRank ниже).

Когда несколько переменных связаны с @-связывающими элементами, они сопоставляются слева направо с соответствующими переменными, связанными с forall, в сигнатуре типа:

const :: forall a. forall b. a -> b -> a
const @ta @tb x  = x

В этом примере @ta соответствует forall a., а @tb соответствует forall b.. Также можно использовать @-связывающие элементы в сочетании с неявным квантификатором (т. е. без явного forall в сигнатуре):

const :: a -> b -> a
const @ta @tb x  = x

В таких случаях переменные типа в сигнатуре считаются квантифицированными с неявным forall в порядке их появления в сигнатуре, см. TypeApplications.

Невозможно сопоставить конкретный тип (например, Maybe или Int) в @-связывающем элементе. Связывающий элемент должен быть безусловным, т. е. он может принимать одну из следующих форм:

• шаблон переменной типа @a
• шаблон переменной типа с аннотацией вида @(f :: Type -> Type)
• подстановка @_, с аннотацией вида или без неё

Основное преимущество использования @-связывающих элементов по сравнению с ScopedTypeVariables заключается в возможности их использования в лямбда-выражениях, передаваемых функциям более высокого ранга:

higherRank :: (forall a. (Num a, Bounded a) => a -> a) -> (Int8, Int16)
higherRank f = (f 42, f 42)

ex :: (Int8, Int16)
ex = higherRank (\ @a x -> maxBound @a - x )
                   -- @a-binder in a lambda pattern in an argument
                   -- to a higher-order function

В настоящее время @-связывающий элемент допустим только в ограниченном наборе обстоятельств:

• В левой части функции, где функция должна иметь явную сигнатуру типа:

  f1 :: forall a. a -> forall b. b -> (a, b)
  f1 @a x @b y = (x :: a, y :: b)        -- OK
  

  Было бы незаконно опустить сигнатуру типа для f, также нельзя переместить связывающий элемент в лямбда-выражение в правой части:

  f2 :: forall a. a -> forall b. b -> (a, b)
  f2 = \ @a x @b y -> (x :: a, y :: b)   -- ILLEGAL
  

• В лямбда-выражении с аннотированной встроенной сигнатурой типа:

  f3 = (\ @a x @b y -> (x :: a, y :: b) )      -- OK
      :: forall a. a -> forall b. b -> (a, b)
  

• В лямбда-выражении, используемом в качестве аргумента функции или конструктора данных более высокого ранга:

  h :: (forall a. a -> forall b. b -> (a, b)) -> (Int, Bool)
  h = ...
  
  f4 = h (\ @a x @b y -> (x :: a, y :: b))     -- OK
  

• В лямбда-выражении, используемом в качестве поля структуры данных (например, элемент списка), тип которой непредсказуем (см. ImpredicativeTypes):

  f5 :: [forall a. a -> a -> a]
  f5 = [ \ @a x _ -> x :: a,
         \ @a _ y -> y :: a ]
  

• В лямбда-выражении с несколькими аргументами, где первый аргумент виден, и только если DeepSubsumption выключен:

  {-# LANGUAGE NoDeepSubsumption #-}
  f6 :: () -> forall a. a -> (a, a)
  f6 = \ _ @a x -> (x :: a, x)   -- OK
  

6.4.17.3. Невидимые связывающие элементы в объявлениях типов

Since: GHC 9.8

type C :: forall k. k -> Constraint
class C @k a where ...
        ^^

type D :: forall k j. k -> j -> Type
data D @k @j (a :: k) (b :: j) = ...
       ^^ ^^

type F :: forall p q. p -> q -> (p, q)
type family F @p @q a b where ...
              ^^ ^^

type F :: forall p q. p -> q -> (p, q)
type family F @(p :: Type) @(q :: Type) (a :: p) (b :: q) where ...

type C :: forall i. (i -> i -> i) -> Constraint
class C @i a where
    p :: P a i

type B :: forall k. k -> forall j. j -> Type
data B @k (a :: k) @j (b :: j)

type S :: forall a b. a -> b -> Type
type S @k x y = ...

-- Inferred kind: forall k. k -> forall j. j -> Type
data B @(k :: Type) (a :: k) @(j :: Type) (b :: j)

6.4.17.4. Подстановки подстановочных знаков в объявлениях типов

С момента: GHC 9.12

Связанные переменные типов, которые не используются, могут быть заменены подстановочными знаками:

type UConst a b = a   -- unused named binder `b`
type WConst a _ = a   -- wildcard binder

Точно так же, как и связанная переменная с именем, подстановка подстановочного знака _ может быть:

• простой: _
• с указанием типа: (_ :: k -> Type)
• скрытой, простой: @_
• скрытой, с указанием типа: @(_ :: k -> Type)

Подстановки подстановочных знаков и абстракции типов, в принципе, являются отдельными функциями. Однако оба они включены в расширение TypeAbstractions для удобства администрирования. Эти две функции могут использоваться вместе для пропуска префикса скрытых переменных типов:

type D :: forall k1 k2 k3. k1 -> k2 -> k3 -> Type
data D @_ @_ @k3 a b c = ...

В данном примере нас интересует k3 и используются подстановочные знаки @_ для избежания связывания k1 и k2.