GADT syntax

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.