6.4.7. Declaring data types with explicit constructor signatures¶

GADTSyntax
¶  Since
7.2.1
Allow the use of GADT syntax in data type definitions (but not GADTs themselves; for this see
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
The form is called a “GADTstyle declaration” because Generalised Algebraic Data Types, described in Generalised Algebraic Data Types (GADTs), can only be declared using this form.
Notice that GADTstyle syntax generalises existential types (Existentially quantified data constructors). For example, these two declarations are equivalent:
data Foo = forall a. MkFoo a (a > Bool)
data Foo' where { MKFoo :: a > (a>Bool) > Foo' }
Any data type that can be declared in standard Haskell 98 syntax can also be declared using GADTstyle syntax. The choice is largely stylistic, but GADTstyle declarations differ in one important respect: they treat class constraints on the data constructors differently. Specifically, if the constructor is given a typeclass 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 patternmatching 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
patternmatching that dictionary becomes available for the righthand
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
Existentials and type classes. 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, patternmatching on
MkSet'
requires an (Eq a)
constraint! GHC faithfully
implements this behaviour, odd though it is. But for GADTstyle
declarations, GHC’s behaviour is much more useful, as well as much more
intuitive.
6.4.7.1. Formal syntax for GADTs¶
To make more precise what is and what is not permitted inside of a GADTstyle constructor, we provide a BNFstyle grammar for GADT below. Note that this grammar is subject to change in the future.
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>
 '!'
 '~'
Where:
btype
is a type that is not allowed to have an outermostforall
/=>
unless it is surrounded by parentheses. For example,forall a. a
andEq a => a
are not legalbtype
s, but(forall a. a)
and(Eq a => a)
are legal.ctype
is abtype
that has no restrictions on an outermostforall
/=>
, soforall a. a
andEq a => a
are legalctype
s.return_type
is a type that is not allowed to haveforall
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 likeMkT :: Int > forall a. a > T
would be rejected.) As a result,gadt_sig
puts all of its quantification and constraints up front withopt_forall
andopt_context
. Note that higherrankforall
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 likeMkS :: Int > (forall a. a) > S
is allowed, since parentheses separate theforall
from the>
.)Furthermore, GADT constructors do not permit outermost parentheses that surround the
opt_forall
oropt_ctxt
, if at least one of them are used. For example,MkU :: (forall a. a > U)
would be rejected, since it would treat theforall
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 isMkV2 :: forall a. (a > V2)
.The function arrows in a
prefix_gadt_body
, as well as the function arrow in arecord_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
andprefix_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 beC
, and since GHC requires that the return type must be headed byB
, 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 writtenInt
.
6.4.7.2. GADT syntax odds and ends¶
The rest of this section gives further details about GADTstyle 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
, wherea1 ... an
are distinct type variables, then the data type is ordinary; otherwise is a generalised data type (Generalised Algebraic Data Types (GADTs)).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
andT2
: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 universallyquantified 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; theEq
constraint arising from the use of==
is discharged by the pattern match onT1
and similarly theShow
constraint arising from the use ofshow
.Unlike a Haskell98style 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 GADTstyle data type declaration. For example, these two declarations are equivalentdata 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 thedata Foo
in Existentially quantified data constructors.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 GADTstyle 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 fieldf
must be the same (modulo alpha conversion). TheChild
constructor above shows that the signature may have a context, existentiallyquantified variables, and strictness annotations, just as in the nonrecord case. (NB: the “type” that follows the doublecolon 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 GADTstyle 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 Haskell98like record syntax (Record Constructors), recordselector functions are generated only for those fields that have welltyped selectors. Here is the example of that section, in GADTstyle 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 GADTstyle 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 derivedshow
.) So GHC implements the following design: a data constructor declared in a GADTstyle data type declaration is displayed infix byShow
iff (a) it is an operator symbol, (b) it has two arguments, (c) it has a programmersupplied fixity declaration. For exampleinfix 6 (::) data T a where (::) :: Int > Bool > T Int