GADT syntax

PartialTypeSignatures
LambdaCase
Contents
Tags
Implication graph
GADTs GADTSyntax

The GADTSyntax extension allows you to write data declarations in such a way that the types of the constructors are made more obvious.

The name “GADT syntax” comes from the fact that this syntax is necessary when defining GADTs, or generalized algebraic datatypes, but you don’t need to worry about what GADTs are to use the syntax. The GADTs extension implies the GADTSyntax extension; that is, enabling GADTs turns GADTSyntax on as well, but the opposite is not true. When GADTSyntax is enabled but not GADTs, then some features of GADTs are not enabled. We will not concern ourselves with those features in this article.

The extensionGHC documentation for GADTSyntax was introducedGADTs (and thus GADT syntax) existed as early as GHC 6.4, but GADTSyntax was not a separate extension at first. in GHC 7.2.1 and is available in all subsequent GHC releases.

Example: Maybe

Here is the standard definition of Maybe:

data Maybe a = Nothing | Just a

A constructor has a type, just like any other value in Haskell. We can see this in the REPL using the :type command:

λ> :type Nothing
Nothing :: Maybe a

λ> :type Just
Just :: a -> Maybe a

With GADT syntax, we define a type by explicitly writing the type signature for each of its constructors.

{-# LANGUAGE GADTSyntax #-}

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

This definition of Maybe has exactly the same meaning as the one above.

This is why we sometimes use this extension for teaching and learning purposes. It is important to understanding Haskell to understand data constructors as functions. Sometimes, as with Nothing or the Boolean values True and False, they are nullary functions. However, writing our data declaration this way still allows us to notice that Nothing, unlike those Boolean values, is still parameterized by the type variable a. That isn’t visible in the Nothing value at term-level, and we believe it is less obvious when written in standard data declaration syntax (even though the meaning of that and this are identical).

Example: Tuple

Any data declaration that can be written in standard Haskell98 style can be written with GADT syntax.

For example, you could define a heterogeneous pair type resembling a two-tuple.

data Tuple a b where
    Tuple :: a -> b -> Tuple a b
    deriving Show

Note that the Tuple constructor and the (,) constructor then have the same type, albeit without the special syntax.

λ> :type Tuple
Tuple :: a -> b -> Tuple a b

λ> :type (,)
(,) :: a -> b -> (a, b)

Record syntax

You can also use this syntax to define record types. For example, consider this ordinary Person type.

data Person = Person { name :: String, age :: Int }
    deriving Show

The same type written with GADT syntax looks like this (we’ll give it slightly different names so we can have both in scope at once without them clashing):

data Person' where
    Person' :: { name' :: String, age' :: Int } -> Person'
    deriving Show

Just to demonstrate to ourselves that these behave the same way, let’s do a few experiments in our REPL.

The constructors have the same type:

λ> :type Person
Person :: String -> Int -> Person

λ> :type Person'
Person' :: String -> Int -> Person'

And the field accessor functions work just the same:

λ> alonzo = Person "Alonzo" 7
alonzo :: Person

λ> name alonzo
"Alonzo"

λ> age alonzo
7

λ> melman = Person' "Melman" 5
melman :: Person'

λ> name' melman
"Melman"

λ> age' melman
5

There are many more powerful things you can do with GADTs themselves, but this extension only enables the syntax without enabling those other things, so as you become a more experienced Haskeller, you will probably not have much cause to use this extension. But, again, we sometimes find the explicitness of writing the constructors this way helpful when learning, and starting here is also a reasonable gateway to GADTs themselves because you grow accustomed to the funky syntax.

Join Type Classes for courses and projects to get you started and make you an expert in FP with Haskell.