.. _gadt-style:
Declaring data types with explicit constructor signatures
---------------------------------------------------------
.. extension:: GADTSyntax
:shortdesc: Enable generalised algebraic data type syntax.
:implied by: :extension:`GADTs`
:since: 7.2.1
:status: Included in :extension:`GHC2021`
Allow the use of GADT syntax in data type definitions (but not GADTs
themselves; for this see :extension:`GADTs`)
When the ``GADTSyntax`` extension is enabled, GHC allows you to declare
an algebraic data type by giving the type signatures of constructors
explicitly. For example: ::
data Maybe a where
Nothing :: Maybe a
Just :: a -> Maybe a
newtype Down a where
Down :: a -> Down a
The form is called a "GADT-style declaration" because Generalised
Algebraic Data Types, described in :ref:`gadt`, can only be declared
using this form.
Notice that GADT-style syntax generalises existential types
(:ref:`existential-quantification`). For example, these two declarations
are equivalent: ::
data Foo = forall a. MkFoo a (a -> Bool)
data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }
Any datatype (or newtype) that can be declared in standard Haskell 98 syntax,
can also be declared using GADT-style syntax. The choice is largely
stylistic, but GADT-style declarations differ in one important respect:
they treat class constraints on the data constructors differently.
Specifically, if the constructor is given a type-class context, that
context is made available by pattern matching. For example: ::
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)
A use of ``MkSet`` as a constructor (e.g. in the definition of
``makeSet``) gives rise to a ``(Eq a)`` constraint, as you would expect.
The new feature is that pattern-matching on ``MkSet`` (as in the
definition of ``insert``) makes *available* an ``(Eq a)`` context. In
implementation terms, the ``MkSet`` constructor has a hidden field that
stores the ``(Eq a)`` dictionary that is passed to ``MkSet``; so when
pattern-matching that dictionary becomes available for the right-hand
side of the match. In the example, the equality dictionary is used to
satisfy the equality constraint generated by the call to ``elem``, so
that the type of ``insert`` itself has no ``Eq`` constraint.
For example, one possible application is to reify dictionaries: ::
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
Here, a value of type ``NumInst a`` is equivalent to an explicit
``(Num a)`` dictionary.
All this applies to constructors declared using the syntax of
:ref:`existential-with-context`. For example, the ``NumInst`` data type
above could equivalently be declared like this: ::
data NumInst a
= Num a => MkNumInst (NumInst a)
Notice that, unlike the situation when declaring an existential, there
is no ``forall``, because the ``Num`` constrains the data type's
universally quantified type variable ``a``. A constructor may have both
universal and existential type variables: for example, the following two
declarations are equivalent: ::
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
All this behaviour contrasts with Haskell 98's peculiar treatment of
contexts on a data type declaration (Section 4.2.1 of the Haskell 98
Report). In Haskell 98 the definition ::
data Eq a => Set' a = MkSet' [a]
gives ``MkSet'`` the same type as ``MkSet`` above. But instead of
*making available* an ``(Eq a)`` constraint, pattern-matching on
``MkSet'`` *requires* an ``(Eq a)`` constraint! GHC faithfully
implements this behaviour, odd though it is. But for GADT-style
declarations, GHC's behaviour is much more useful, as well as much more
intuitive.
Note that the restrictions of :ref:`existential-restrictions` are still
in place; for example, a newtype declared with ``GADTSyntax`` cannot
use existential quantification.
.. _formal-gadt-syntax:
Formal syntax for GADTs
~~~~~~~~~~~~~~~~~~~~~~~
To make more precise what is and what is not permitted inside of a GADT-style
constructor, we provide a BNF-style grammar for GADT below. Note that this
grammar is subject to change in the future.
.. code-block:: none
gadt_con ::= conids '::' opt_forall opt_ctxt gadt_body
conids ::= conid
| conid ',' conids
opt_forall ::=
| 'forall' tv_bndrs '.'
tv_bndrs ::=
| tv_bndr tv_bndrs
tv_bndr ::= tyvar
| '(' tyvar '::' ctype ')'
opt_ctxt ::=
| 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 ::=
| 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 ::=
| '!'
| '~'
Where:
- ``btype`` is a type that is not allowed to have an outermost
``forall``/``=>`` unless it is surrounded by parentheses. For example,
``forall a. a`` and ``Eq a => a`` are not legal ``btype``\ s, but
``(forall a. a)`` and ``(Eq a => a)`` are legal.
- ``ctype`` is a ``btype`` that has no restrictions on an outermost
``forall``/``=>``, so ``forall a. a`` and ``Eq a => a`` are legal ``ctype``\ s.
- ``return_type`` is a type that is not allowed to have ``forall``\ s, ``=>``\ s,
or ``->``\ s.
This is a simplified grammar that does not fully delve into all of the
implementation details of GHC's parser (such as the placement of Haddock
comments), but it is sufficient to attain an understanding of what is
syntactically allowed. Some further various observations about this grammar:
- GADT constructor types are currently not permitted to have nested ``forall``\ s
or ``=>``\ s. (e.g., something like ``MkT :: Int -> forall a. a -> T`` would be
rejected.) As a result, ``gadt_sig`` puts all of its quantification and
constraints up front with ``opt_forall`` and ``opt_context``. Note that
higher-rank ``forall``\ s and ``=>``\ s are only permitted if they do not appear
directly to the right of a function arrow in a `prefix_gadt_body`. (e.g.,
something like ``MkS :: Int -> (forall a. a) -> S`` is allowed, since
parentheses separate the ``forall`` from the ``->``.)
- Furthermore, GADT constructors do not permit outermost parentheses that
surround the ``opt_forall`` or ``opt_ctxt``, if at least one of them are
used. For example, ``MkU :: (forall a. a -> U)`` would be rejected, since
it would treat the ``forall`` as being nested.
Note that it is acceptable to use parentheses in a ``prefix_gadt_body``.
For instance, ``MkV1 :: forall a. (a) -> (V1)`` is acceptable, as is
``MkV2 :: forall a. (a -> V2)``.
- The function arrows in a ``prefix_gadt_body``, as well as the function
arrow in a ``record_gadt_body``, are required to be used infix. For
example, ``MkA :: (->) Int A`` would be rejected.
- GHC uses the function arrows in a ``prefix_gadt_body`` and
``prefix_gadt_body`` to syntactically demarcate the function and result
types. Note that GHC does not attempt to be clever about looking through
type synonyms here. If you attempt to do this, for instance: ::
type C = Int -> B
data B where
MkB :: C
Then GHC will interpret the return type of ``MkB`` to be ``C``, and since
GHC requires that the return type must be headed by ``B``, this will be
rejected. On the other hand, it is acceptable to use type synonyms within
the argument and result types themselves, so the following is permitted: ::
type B1 = Int
type B2 = B
data B where
MkB :: B1 -> B2
- GHC will accept any combination of ``!``/``~`` and
``{-# UNPACK #-}``/``{-# NOUNPACK #-}``, although GHC will ignore some
combinations. For example, GHC will produce a warning if you write
``{-# UNPACK #-} ~Int`` and proceed as if you had written ``Int``.
GADT syntax odds and ends
~~~~~~~~~~~~~~~~~~~~~~~~~
The rest of this section gives further details about GADT-style data
type declarations.
- The result type of each data constructor must begin with the type
constructor being defined. If the result type of all constructors has
the form ``T a1 ... an``, where ``a1 ... an`` are distinct type
variables, then the data type is *ordinary*; otherwise is a
*generalised* data type (:ref:`gadt`).
- As with other type signatures, you can give a single signature for
several data constructors. In this example we give a single signature
for ``T1`` and ``T2``: ::
data T a where
T1,T2 :: a -> T a
T3 :: T a
- The type signature of each constructor is independent, and is
implicitly universally quantified as usual. In particular, the type
variable(s) in the "``data T a where``" header have no scope, and
different constructors may have different universally-quantified type
variables: ::
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
- A constructor signature may mention type class constraints, which can
differ for different constructors. For example, this is fine: ::
data T a where
T1 :: Eq b => b -> b -> T b
T2 :: (Show c, Ix c) => c -> [c] -> T c
When pattern matching, these constraints are made available to
discharge constraints in the body of the match. For example: ::
f :: T a -> String
f (T1 x y) | x==y = "yes"
| otherwise = "no"
f (T2 a b) = show a
Note that ``f`` is not overloaded; the ``Eq`` constraint arising from
the use of ``==`` is discharged by the pattern match on ``T1`` and
similarly the ``Show`` constraint arising from the use of ``show``.
- Unlike a Haskell-98-style data type declaration, the type variable(s)
in the "``data Set a where``" header have no scope. Indeed, one can
write a kind signature instead: ::
data Set :: Type -> Type where ...
or even a mixture of the two: ::
data Bar a :: (Type -> Type) -> Type where ...
The type variables (if given) may be explicitly kinded, so we could
also write the header for ``Foo`` like this: ::
data Bar a (b :: Type -> Type) where ...
- You can use strictness annotations, in the obvious places in the
constructor type: ::
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)
- You can use a ``deriving`` clause on a GADT-style data type
declaration. For example, these two declarations are equivalent ::
data Maybe1 a where {
Nothing1 :: Maybe1 a ;
Just1 :: a -> Maybe1 a
} deriving( Eq, Ord )
data Maybe2 a = Nothing2 | Just2 a
deriving( Eq, Ord )
- The type signature may have quantified type variables that do not
appear in the result type: ::
data Foo where
MkFoo :: a -> (a->Bool) -> Foo
Nil :: Foo
Here the type variable ``a`` does not appear in the result type of
either constructor. Although it is universally quantified in the type
of the constructor, such a type variable is often called
"existential". Indeed, the above declaration declares precisely the
same type as the ``data Foo`` in :ref:`existential-quantification`.
The type may contain a class context too, of course: ::
data Showable where
MkShowable :: Show a => a -> Showable
- You can use record syntax on a GADT-style data type declaration: ::
data Person where
Adult :: { name :: String, children :: [Person] } -> Person
Child :: Show a => { name :: !String, funny :: a } -> Person
As usual, for every constructor that has a field ``f``, the type of
field ``f`` must be the same (modulo alpha conversion). The ``Child``
constructor above shows that the signature may have a context,
existentially-quantified variables, and strictness annotations, just
as in the non-record case. (NB: the "type" that follows the
double-colon is not really a type, because of the record syntax and
strictness annotations. A "type" of this form can appear only in a
constructor signature.)
- Record updates are allowed with GADT-style declarations, only fields
that have the following property: the type of the field mentions no
existential type variables.
- As in the case of existentials declared using the Haskell-98-like
record syntax (:ref:`existential-records`), record-selector functions
are generated only for those fields that have well-typed selectors.
Here is the example of that section, in GADT-style syntax: ::
data Counter a where
NewCounter :: { _this :: self
, _inc :: self -> self
, _display :: self -> IO ()
, tag :: a
} -> Counter a
As before, only one selector function is generated here, that for
``tag``. Nevertheless, you can still use all the field names in
pattern matching and record construction.
- In a GADT-style data type declaration there is no obvious way to
specify that a data constructor should be infix, which makes a
difference if you derive ``Show`` for the type. (Data constructors
declared infix are displayed infix by the derived ``show``.) So GHC
implements the following design: a data constructor declared in a
GADT-style data type declaration is displayed infix by ``Show`` iff
(a) it is an operator symbol, (b) it has two arguments, (c) it has a
programmer-supplied fixity declaration. For example
::
infix 6 (:--:)
data T a where
(:--:) :: Int -> Bool -> T Int