GADT syntax

Contents

Example: Maybe

The GADTSyntax extension allows you to write data declarations so that the types of the constructors are made more obvious. This is a great reminder while you’re learning.

The name “GADT syntax” comes from the fact that it was introduced for the purpose of defining GADTs, but you don’t need to worry about what GADTs are to use the 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.

Type Classes offers courses and projects to get you started and make you an expert in FP with Haskell. For $29/month, you get access to the complete archive and all the latest content.

GADT syntax

Example: Maybe

Example: `Maybe`