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

GADTSyntax

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

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

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

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

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

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

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

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

Любой тип данных (или newtype), который можно объявить в стандартном синтаксисе 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 гораздо полезнее и интуитивнее.

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

6.4.8.1. Формальный синтаксис GADT

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

gadt_con ::= conids '::' foralls opt_ctxt gadt_body

conids ::= conid
        |  conid ',' conids

foralls ::= <empty>
         | forall_telescope foralls

forall_telescope ::= 'forall' tv_bndrs_spec '.'
                  |  'forall' tv_bndrs      '->'   -- with RequiredTypeArguments

tv_bndrs      ::= <empty> | tv_bndr      tv_bndrs
tv_bndrs_spec ::= <empty> | tv_bndr_spec tv_bndrs_spec

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

tv_bndr_spec  ::= 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 указывает всю квантификацию и ограничения в начале с помощью foralls и opt_context. Обратите внимание, что forall и => более высокого ранга разрешены, только если они не стоят непосредственно справа от стрелки функции в prefix_gadt_body. (Например, выражение вида MkS :: Int -> (forall a. a) -> S допустимо, поскольку скобки отделяют forall от ->.)
Кроме того, для конструкторов GADT не разрешены внешние скобки, охватывающие foralls или 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.8.2. Дополнительные замечания о синтаксисе GADT

В оставшейся части раздела приводятся дополнительные сведения об объявлениях типов данных в стиле GADT.

Тип результата каждого конструктора данных должен начинаться с определяемого конструктора типа. Если тип результата всех конструкторов имеет вид T a1 ... an, где a1 ... an — различные переменные типа, то тип данных является обычным; в противном случае это обобщённый тип данных (Обобщённые алгебраические типы данных (GADT)).
Как и для других сигнатур типов, можно задать одну сигнатуру для нескольких конструкторов данных. В этом примере одна сигнатура задаётся для 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)

В объявлении типа данных в стиле GADT можно использовать предложение deriving. Например, следующие два объявления эквивалентны:
```
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.14.1/docs/users_guide/exts/gadt_syntax.html