6.4.7. Объявление типов данных со явными сигнатурами конструкторов

GADTSyntax

Подразумевается:: GADTs
С момента:: 7.2.1
Статус:: Включено в GHC2024, GHC2021

Разрешает использовать синтаксис GADT в определениях типов данных (но не сами GADTs; для этого см. GADTs)

Когда расширение GADTSyntax включено, GHC позволяет объявлять алгебраический тип данных, явно указывая сигнатуры типов конструкторов. Например:

data Maybe a where
    Nothing :: Maybe a
    Just    :: a -> Maybe a

newtype Down a where
  Down :: a -> Down a

Такая форма называется «объявлением в стиле GADT», потому что обобщённые алгебраические типы данных, описанные в Обобщённые алгебраические типы данных (GADTs), могут быть объявлены только с помощью этой формы.

Обратите внимание, что синтаксис в стиле GADT обобщает экзистенциальные типы (Экзистенциально квантованные конструкторы данных). Например, эти два объявления эквивалентны:

data Foo = forall a. MkFoo a (a -> Bool)
data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }

Любой тип данных (или новый тип), который может быть объявлен в стандартном синтаксисе Haskell 98, также может быть объявлен с использованием синтаксиса в стиле GADT. Выбор в основном стилистический, но объявления в стиле GADT отличаются в одном важном аспекте: они по-разному обрабатывают ограничения классов для конструкторов данных. В частности, если конструктор получает контекст класса типов, этот контекст становится доступным при сопоставлении с образцом. Например:

data Set a where
  MkSet :: Eq a => [a] -> Set a

makeSet :: Eq a => [a] -> Set a
makeSet xs = MkSet (nub xs)

insert :: a -> Set a -> Set a
insert a (MkSet as) | a `elem` as = MkSet as
                    | otherwise   = MkSet (a:as)

Использование MkSet как конструктора (например, в определении makeSet) приводит к ограничению (Eq a), как и ожидалось. Новая особенность заключается в том, что сопоставление с образцом на MkSet (как в определении insert) делает доступным контекст (Eq a). С точки зрения реализации, конструктор MkSet имеет скрытое поле, хранящее словарь (Eq a), который передаётся в MkSet; поэтому при сопоставлении с образцом этот словарь становится доступным для правой части сопоставления. В примере словарь равенства используется для удовлетворения ограничения равенства, сгенерированного вызовом elem, таким образом, тип insert сам по себе не имеет ограничения Eq.

Например, одно возможное применение заключается в реификационной словарей:

data NumInst a where
  MkNumInst :: Num a => NumInst a

intInst :: NumInst Int
intInst = MkNumInst

plus :: NumInst a -> a -> a -> a
plus MkNumInst p q = p + q

Здесь значение типа NumInst a эквивалентно явным словарю (Num a).

Всё это относится к конструкторам, объявленным с помощью синтаксиса Экзистенциальные объекты и классы типов. Например, тип данных NumInst выше можно эквивалентно объявить так:

data NumInst a
   = Num a => MkNumInst (NumInst a)

Обратите внимание, что, в отличие от ситуации при объявлении экзистенциального типа, здесь нет forall, поскольку Num ограничивает универсальную квантифицированную переменную типа a типа данных. Конструктор может иметь как универсальные, так и экзистенциальные переменные типа: например, следующие два объявления эквивалентны:

data T1 a
 = forall b. (Num a, Eq b) => MkT1 a b
data T2 a where
 MkT2 :: (Num a, Eq b) => a -> b -> T2 a

Всё это поведение отличается от специфичного обращения Haskell 98 с контекстами в объявлении типа данных (раздел 4.2.1 отчета Haskell 98). В Haskell 98 определение

data Eq a => Set' a = MkSet' [a]

присваивает MkSet' тот же тип, что и MkSet выше. Но вместо того, чтобы делать доступным ограничение (Eq a), сопоставление с образцом на MkSet' требует ограничения (Eq a)! GHC исправно реализует это поведение, хоть оно и странное. Но для объявлений в стиле GADT поведение GHC гораздо более полезно и интуитивно понятно.

Обратите внимание, что ограничения Ограничения всё ещё действуют; например, новый тип, объявленный с помощью GADTSyntax не может использовать экзистенциальное квантование.

6.4.7.1. Формальный синтаксис для GADTs

Чтобы точнее определить, что разрешается, а что нет внутри конструктора в стиле GADT, мы предоставляем грамматику в стиле БНФ для GADT ниже. Обратите внимание, что эта грамматика может быть изменена в будущем.

gadt_con ::= conids '::' opt_forall opt_ctxt gadt_body

conids ::= conid
        |  conid ',' conids

opt_forall ::= <empty>
            |  'forall' tv_bndrs '.'

tv_bndrs ::= <empty>
          |  tv_bndr tv_bndrs

tv_bndr ::= tyvar
         |  '(' tyvar '::' ctype ')'

opt_ctxt ::= <empty>
          |  btype '=>'
          |  '(' ctxt ')' '=>'

ctxt ::= ctype
      |  ctype ',' ctxt

gadt_body ::= prefix_gadt_body
           |  record_gadt_body

prefix_gadt_body ::= '(' prefix_gadt_body ')'
                  |  return_type
                  |  opt_unpack btype '->' prefix_gadt_body

record_gadt_body ::= '{' fieldtypes '}' '->' return_type

fieldtypes ::= <empty>
            |  fieldnames '::' opt_unpack ctype
            |  fieldnames '::' opt_unpack ctype ',' fieldtypes

fieldnames ::= fieldname
            |  fieldname ',' fieldnames

opt_unpack ::= opt_bang
            :  {-# UNPACK #-} opt_bang
            |  {-# NOUNPACK #-} opt_bang

opt_bang ::= <empty>
          |  '!'
          |  '~'

Где:

btype — это тип, которому не разрешено иметь внешний forall/=>, если он не окружён скобками. Например, forall a. a и Eq a => a не являются допустимыми btypeами, но (forall a. a) и (Eq a => a) являются допустимыми.
ctype — это btype, которому не накладываются ограничения на внешний forall/=>, поэтому forall a. a и Eq a => a являются допустимыми ctypeами.
return_type — это тип, которому не разрешено содержать forallы, =>ы или ->ы.

Это упрощённая грамматика, которая не полностью раскрывает все детали реализации парсера GHC (например, расположение комментариев Haddock), но её достаточно, чтобы понять, что синтаксически разрешено. Некоторые дополнительные наблюдения по этой грамматике:

В настоящее время для типов конструкторов GADT не разрешено иметь вложенные forallы или =>ы. (Например, что-то вроде MkT :: Int -> forall a. a -> T будет отклонено.) В результате gadt_sig помещает всю квантификацию и ограничения вначале с помощью opt_forall и opt_context . Обратите внимание, что высшего порядка forallы и =>ы разрешаются только в том случае, если они не появляются непосредственно справа от стрелки функции в prefix_gadt_body. (Например, что-то вроде MkS :: Int -> (forall a. a) -> S разрешено, так как скобки отделяют forall от ->.)
Кроме того, конструкторы GADT не допускают внешних скобок, окружающих opt_forall или opt_ctxt, если хотя бы один из них используется. Например, MkU :: (forall a. a -> U) будет отклонено, так как это будет рассматривать forall как вложенный.

Обратите внимание, что использование скобок в prefix_gadt_body допустимо. Например, MkV1 :: forall a. (a) -> (V1) допустимо, как и MkV2 :: forall a. (a -> V2).
Стрелки функций в prefix_gadt_body, а также стрелка функции в record_gadt_body, должны использоваться инфиксным способом. Например, MkA :: (->) Int A будет отклонено.
GHC использует стрелки функций в prefix_gadt_body и prefix_gadt_body для синтаксической разметки типов функции и результата. Обратите внимание, что GHC не пытается быть умным, просматривая синонимы типов здесь. Если вы попытаетесь это сделать, например:
```
type C = Int -> B

data B where
  MkB :: C
```
то GHC интерпретирует тип возвращаемого значения MkB как C, и поскольку GHC требует, чтобы тип возвращаемого значения начинался с B, это будет отклонено. С другой стороны, использование синонимов типов в самих типах аргументов и результата допускается, поэтому следующее разрешено:
```
type B1 = Int
type B2 = B

data B where
  MkB :: B1 -> B2
```
GHC примет любую комбинацию !/~ и {-# UNPACK #-}/{-# NOUNPACK #-}, хотя GHC проигнорирует некоторые комбинации. Например, GHC выдаст предупреждение, если вы напишете {-# UNPACK #-} ~Int и поступите так, как будто вы написали Int.

6.4.7.2. Особенности синтаксиса GADTs

В данном разделе приводятся дополнительные сведения о объявлениях типов данных в стиле GADTs.

Тип результата каждого конструктора данных должен начинаться с типа конструктора, который определяется. Если тип результата всех конструкторов имеет вид T a1 ... an, где a1 ... an - различные переменные типа, то тип данных является обычным; в противном случае это обобщённый тип данных (Обобщённые алгебраические типы данных (GADTs)).
Как и в других сигнатурах типов, вы можете указать одну сигнатуру для нескольких конструкторов данных. В этом примере мы даём одну сигнатуру для T1 и T2:
```
data T a where
  T1,T2 :: a -> T a
  T3 :: T a
```
Сигнатура типа каждого конструктора является независимой и неявно универсально квантифицируется, как обычно. В частности, переменные типа в заголовке «data T a where» не имеют области действия, и разные конструкторы могут иметь разные универсально квантифицированные переменные типа:
```
data T a where        -- The 'a' has no scope
  T1,T2 :: b -> T b   -- Means forall b. b -> T b
  T3 :: T a           -- Means forall a. T a
```
Сигнатура конструктора может упоминать ограничения класса типов, которые могут отличаться для разных конструкторов. Например, это допустимо:
```
data T a where
  T1 :: Eq b => b -> b -> T b
  T2 :: (Show c, Ix c) => c -> [c] -> T c
```
При сопоставлении с образцом эти ограничения становятся доступными для разрешения ограничений в теле сопоставления. Например:
```
f :: T a -> String
f (T1 x y) | x==y      = "yes"
           | otherwise = "no"
f (T2 a b)             = show a
```
Обратите внимание, что f не перегружен; ограничение Eq, возникающее при использовании ==, разрешается при сопоставлении с образцом T1, и аналогично ограничение Show от использования show.
В отличие от объявления типа в стиле Haskell-98, переменные типа в заголовке «data Set a where» не имеют области действия. Действительно, можно написать сигнатуру типа вместо неё:
```
data Set :: Type -> Type where ...
```
или даже смесь двух:
```
data Bar a :: (Type -> Type) -> Type where ...
```
Переменные типа (если указаны) могут быть явно типизированы, поэтому мы также можем записать заголовок для Foo так:
```
data Bar a (b :: Type -> Type) where ...
```
Вы можете использовать аннотации строгости в соответствующих местах в типе конструктора:
```
data Term a where
    Lit    :: !Int -> Term Int
    If     :: Term Bool -> !(Term a) -> !(Term a) -> Term a
    Pair   :: Term a -> Term b -> Term (a,b)
```
Вы можете использовать deriving в объявлении типа данных в стиле GADT. Например, эти два объявления эквивалентны
```
data Maybe1 a where {
    Nothing1 :: Maybe1 a ;
    Just1    :: a -> Maybe1 a
  } deriving( Eq, Ord )

data Maybe2 a = Nothing2 | Just2 a
     deriving( Eq, Ord )
```
Сигнатура типа может содержать квантифицированные переменные типа, которые не появляются в типе результата:
```
data Foo where
   MkFoo :: a -> (a->Bool) -> Foo
   Nil   :: Foo
```
Здесь переменная типа a не появляется в типе результата ни одного конструктора. Хотя она универсально квантифицирована в типе конструктора, такая переменная типа часто называется «экзистенциальной». Действительно, вышеприведённое объявление описывает точно тот же тип, что и data Foo в Экзистенциально квантифицированные конструкторы данных.

Конечно, тип может также содержать контекст класса:
```
data Showable where
  MkShowable :: Show a => a -> Showable
```
Вы можете использовать синтаксис записей в объявлении типа данных в стиле GADT:
```
data Person where
    Adult :: { name :: String, children :: [Person] } -> Person
    Child :: Show a => { name :: !String, funny :: a } -> Person
```
Как обычно, для каждого конструктора, который имеет поле f, тип поля f должен быть одинаковым (с точностью до альфа-преобразования). Конструктор Child выше показывает, что сигнатура может иметь контекст, экзистенциально квантифицированные переменные и аннотации строгости, как и в нерекордном случае. (Примечание: «тип», следующий за двоеточием, фактически не является типом из-за синтаксиса записей и аннотаций строгости. «Тип» в таком виде может появиться только в сигнатуре конструктора.)
Обновления записей разрешены с объявлениями типов в стиле GADT, только для полей, имеющих следующее свойство: тип поля не упоминает никаких экзистенциальных переменных типов.
Как и в случае с экзистенциалами, объявленными с помощью синтаксиса записей в стиле Haskell-98 (Конструкторы записей), функции-селекторы записей генерируются только для тех полей, для которых существуют хорошо типизированные селекторы. Вот пример из того раздела в синтаксисе в стиле GADT:
```
data Counter a where
    NewCounter :: { _this    :: self
                  , _inc     :: self -> self
                  , _display :: self -> IO ()
                  , tag      :: a
                  } -> Counter a
```
Как и прежде, здесь генерируется только одна функция-селектор, для tag. Тем не менее, вы всё ещё можете использовать все имена полей в сопоставлении с образцом и построении записей.
В объявлении типа данных в стиле GADT нет очевидного способа указать, что конструктор данных должен быть инфиксным, что имеет значение, если вы выводите Show для типа. (Конструкторы данных, объявленные инфиксными, отображаются инфиксными функциями вывода show.) Поэтому GHC реализует следующий дизайн: конструктор данных, объявленный в объявлении типа данных в стиле GADT, отображается инфиксным Show тогда и только тогда, когда (а) он является операторным символом, (б) он имеет два аргумента, (в) у него есть объявление фикстуры, заданное программистом. Например
```
infix 6 (:--:)
data T a where
  (:--:) :: Int -> Bool -> T Int
```

© 2002–2007 The University Court of the University of Glasgow. All rights reserved.
Licensed under the Glasgow Haskell Compiler License.
https://downloads.haskell.org/~ghc/9.12.1/docs/users_guide/exts/gadt_syntax.html