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.

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