I like using GADTs in Haskell. However, I find the explanation in the article nearly impossible to understand. This annoys me, so I will attempt to give my own explanation of what GADTs are. (Because everyone else explains it incorrectly and my explanation is of course the best, right? /s)

So, a bit of Haskell first, starting with algebraic data types. (Skip this if you already know about ADTs.) If you want to define a data type in most languages, there are basically two things you can do. Either you can define a record, with multiple values wrapped up as a single type:

    data MyRecord = ConstructorName Int String Bool

Or, you can define an enumeration, where a type has a limited set of allowed values:

    data TrafficLight = Red | Amber | Green

Haskell calls the former ‘product types’ and the latter ‘sum types’.

The thing is, there’s nothing stopping you from combining the two: making an enumeration where each value of the enumeration is a record. This is called an algebraic data type (because it combines sums and products, geddit?) For instance, this lets me make an AST for a simple language:

    data AST
        = Integer Int
        | Boolean Bool
        | Addition AST AST
        | Multiplication AST AST
        | Equals AST AST
        | Not AST

So now I can make values like `Not (Equals (Integer 1) (Integer 2)) :: AST`. (In Haskell, read ‘::’ as ‘has-type’.)

Often, you want to make data types polymorphic over the record field type. For instance, I might have a type expressing either an integer or an error:

    data IntErr = Error String | IntResult Int

And I might have expressing either a string or an error:

    data StrErr = Error String | StrResult Int

And eventually I might get tired of writing out all these types. In that case I can add a type variable representing any type:

    data WithError a = Error String | Result a

So now I can have `Result 3 :: WithError Int`, `Result True :: WithError Bool`, and so on. (This is basically the same as generics or templates in languages which have them.)

The thing is, no-one says a type parameter needs to correspond to anything concrete. There’s nothing in Haskell which stops me from doing this:

    data Weird a b = IgnoreTheType Int

This is a bit weird. If you have a value of type `Weird String Bool`, say, that value won’t actually have a string or a boolean within it. And `IgnoreTheType 1 :: Weird String Bool`, `IgnoreTheType 2 :: Weird Char Float`, `IgnoreTheType 3 :: Weird Bool Double` are all values of different types. You can basically change the type at will without affecting the value. Variables such as `a` and `b` are called ‘phantom type variables’.

Now let’s back up a bit and have another look at that `AST` data type I defined earlier. It’s not particularly satisfying: you can easily create meaningless terms like `Addition (Boolean True) (Not (Integer 3))`. As Haskellers, we want to avoid this as much as possible. So let’s add a phantom type parameter to express the type returned by each `AST` constructor:

    data AST r
        = Integer Int
        | Boolean Bool
        | Addition (AST Int) (AST Int)
        | Multiplication (AST Int) (AST Int)
        | Equals (AST r) (AST r)
        | Not (AST Bool)

This says that multiplication, for instance, must take two `AST`s returning an `Int`, as encoded in the type parameter. But wait — how do we restrict the type parameter? We need to be able to say that something constructed with `Multiplication` must have type `AST Int`, but something constructed with `Not` must have type `AST Bool`. As it happens, vanilla Haskell has no way of doing this. There is no way of explicitly controlling the value of `r` based on which constructor is used.

You might have guessed by now that this is exactly what generalised algebraic data types let us do. And indeed, `AST` can be easily implemented as a GADT:

    data AST r where
        Integer        :: Int -> AST Int
        Boolean        :: Bool -> AST Bool
        Addition       :: AST Int -> AST Int -> AST Int
        Multiplication :: AST Int -> AST Int
        Equals         :: AST r -> AST r -> AST Bool
        Not            :: AST Bool -> AST Bool

And now, if we try to construct an incorrect AST, the compiler will give us back an error, because the types don’t match:

    > Addition (Boolean True) (Not (Integer 3))
    
    <interactive>:11:11: error:
        * Couldn't match type `Bool' with `Int'
          Expected type: AST Int
            Actual type: AST Bool
        * In the first argument of `Addition', namely `(Boolean True)'
          In the expression: Addition (Boolean True) (Not (Integer 3))
          In an equation for `it':
              it = Addition (Boolean True) (Not (Integer 3))
    
    <interactive>:11:26: error:
        * Couldn't match type `Bool' with `Int'
          Expected type: AST Int
            Actual type: AST Bool
        * In the second argument of `Addition', namely `(Not (Integer 3))'
          In the expression: Addition (Boolean True) (Not (Integer 3))
          In an equation for `it':
              it = Addition (Boolean True) (Not (Integer 3))
    
    <interactive>:11:31: error:
        * Couldn't match type `Int' with `Bool'
          Expected type: AST Bool
            Actual type: AST Int
        * In the first argument of `Not', namely `(Integer 3)'
          In the second argument of `Addition', namely `(Not (Integer 3))'
          In the expression: Addition (Boolean True) (Not (Integer 3))