GADTs for Dummies
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 <i>my</i> explanation is of course the best, right? &#x2F;s)<p>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:<p><pre><code>    data MyRecord = ConstructorName Int String Bool
</code></pre>
Or, you can define an enumeration, where a type has a limited set of allowed values:<p><pre><code>    data TrafficLight = Red | Amber | Green
</code></pre>
Haskell calls the former ‘product types’ and the latter ‘sum types’.<p>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 <i>algebraic data type</i> (because it combines sums and products, geddit?) For instance, this lets me make an AST for a simple language:<p><pre><code>    data AST
        = Integer Int
        | Boolean Bool
        | Addition AST AST
        | Multiplication AST AST
        | Equals AST AST
        | Not AST
</code></pre>
So now I can make values like `Not (Equals (Integer 1) (Integer 2)) :: AST`. (In Haskell, read ‘::’ as ‘has-type’.)<p>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:<p><pre><code>    data IntErr = Error String | IntResult Int
</code></pre>
And I might have expressing either a string or an error:<p><pre><code>    data StrErr = Error String | StrResult Int
</code></pre>
And eventually I might get tired of writing out all these types. In that case I can add a <i>type variable</i> representing any type:<p><pre><code>    data WithError a = Error String | Result a
</code></pre>
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.)<p>The thing is, no-one says a type parameter <i>needs</i> to correspond to anything concrete. There’s nothing in Haskell which stops me from doing this:<p><pre><code>    data Weird a b = IgnoreTheType Int
</code></pre>
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’.<p>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:<p><pre><code>    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)
</code></pre>
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.<p>You might have guessed by now that this is exactly what <i>generalised</i> algebraic data types let us do. And indeed, `AST` can be easily implemented as a GADT:<p><pre><code>    data AST r where
        Integer        :: Int -&gt; AST Int
        Boolean        :: Bool -&gt; AST Bool
        Addition       :: AST Int -&gt; AST Int -&gt; AST Int
        Multiplication :: AST Int -&gt; AST Int
        Equals         :: AST r -&gt; AST r -&gt; AST Bool
        Not            :: AST Bool -&gt; AST Bool
</code></pre>
And now, if we try to construct an incorrect AST, the compiler will give us back an error, because the types don’t match:<p><pre><code>    &gt; Addition (Boolean True) (Not (Integer 3))
    
    &lt;interactive&gt;:11:11: error:
        * Couldn&#x27;t match type `Bool&#x27; with `Int&#x27;
          Expected type: AST Int
            Actual type: AST Bool
        * In the first argument of `Addition&#x27;, namely `(Boolean True)&#x27;
          In the expression: Addition (Boolean True) (Not (Integer 3))
          In an equation for `it&#x27;:
              it = Addition (Boolean True) (Not (Integer 3))
    
    &lt;interactive&gt;:11:26: error:
        * Couldn&#x27;t match type `Bool&#x27; with `Int&#x27;
          Expected type: AST Int
            Actual type: AST Bool
        * In the second argument of `Addition&#x27;, namely `(Not (Integer 3))&#x27;
          In the expression: Addition (Boolean True) (Not (Integer 3))
          In an equation for `it&#x27;:
              it = Addition (Boolean True) (Not (Integer 3))
    
    &lt;interactive&gt;:11:31: error:
        * Couldn&#x27;t match type `Int&#x27; with `Bool&#x27;
          Expected type: AST Bool
            Actual type: AST Int
        * In the first argument of `Not&#x27;, namely `(Integer 3)&#x27;
          In the second argument of `Addition&#x27;, namely `(Not (Integer 3))&#x27;
          In the expression: Addition (Boolean True) (Not (Integer 3))</code></pre>