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

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

Начиная с: 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)

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

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

Пример, несколько искусственный:

foo :: (Show a, 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

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

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

Начиная с: 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.18.3. Невидимые связыватели в объявлениях типов

Начиная с: 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.18.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.