GADT syntax

Contents
Tags

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.

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