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.
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