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

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))