GADTs for Dummies (wiki.haskell.org)

Once you understand their basics, GADTs are as easy to use as any other mainstream language feature. I wonder if any mainstream language will meaningfully have them soon. Not technically (many do) but meaningfully. Lightweight syntax and fully-powered pattern matching.

    type Term = {kind: 'lit', value: number} | {kind: 'pair', left: Term, right: Term};

    function pair(left: Term, right: Term): Term & {kind: 'pair'} {
        return {kind: 'pair', left, right};
    }
    function lit(n: number): Term & {kind: 'lit'} {
        return {kind: 'lit', value: n};
    }
    let t: Term =  pair(
        pair(lit(1), lit(2)),
        lit(3)
    );

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

    enum MyRecord {
      ConstructorName(Int, String, Bool)
    }

    enum TrafficLight {
      Red,
      Yellow,
      Green
    }

    enum AST {
      Integer(Int),
      Boolean(Bool),
      Addition(Ast, Ast),
      Multiplication(Ast, Ast),
      Equals(Ast, Ast),
      Not(Ast)
    }

    enum IntErr {
      Error(String),
      IntResult(Int)
    }

    enum StringErr {
      Error(String),
      StringResult(String)
    }

    enum WithError<A> {
      Error(String),
      Result(A)
    }

    enum Weird<A, B> {
      IgnoreTheType(Int),
    }

    enum AST<R> {
      Integer(Int),
      Boolean(Bool),
      Addition(Ast<Int>, Ast<Int>),
      Multiplication(Ast<Int>, Ast<Int>),
      Equals(Ast<R>, Ast<R>),
      Not(Ast<Bool>)
    }

    enum AST<R> {
      Integer(Int) : Ast<Int>,
      Boolean(Bool) : Ast<Bool>,
      Addition(Ast<Int>, Ast<Int>) : Ast<Int>,
      Multiplication(Ast<Int>, Ast<Int>) : Ast<Int>,
      Equals(Ast<R>, Ast<R>) : Ast<Bool>,
      Not(Ast<Bool>) : Ast<Bool>
    }

I like that GADTs are a good example of "lightweight dependent types". You don't need to use full-blown dependent types to achieve the following:

- type-safe AST representations of a language

- type-safe encoding of lambda calculus and an eval function that will only accept _closed terms_ (i.e. no free variables!)

In Coq, everything is defined in the GADT style and with dependent types you have an explosion of possibilities:

- length-indexed vectors

- dependently-typed red-black trees

- inductive proofs!

just to name a few.

Somewhat related: What has blown my mind at some point is that with dependent types you can actually check your algorithms for correctness.

---

Example: http://goto.ucsd.edu:8090/index.html#?demo=Order.hs

Press Check -> The button should turn green and say "Safe"

Now mess up the algorithm, e.g. change the `>=` in line 174 to `<=` in effect changing the sorting order.

Press Check again -> The button should turn red and the line you changed should be highlighted telling you that at this point you violated the ordering constraint that put in place by the `IncrList a` type.

---

To be fair, I don't think too many programming work is low-level algorithmic programming where this would be applicable.

I see the benefits in having type level size constraints on arrays or having a "Safe / Unsafe" constraint on input from users that can only be changed by running through verification functions.

Understanding how GADT works only comes next to understanding how leveraging the typing system during design can be beneficial. The motivation to go through this tutorial stems from the desire to let the typing system strengthen the programs and API. I'm coming from the Java world and I've spent some time learning Haskell for my own culture. At the time, I was trying to use Java generics to encode some restrictions in my design. It was interesting but alas a bit limited by the Java generics implementation and the results were most of the time hard to use or understand.

I'd like to see more articles on how GADT (or any other mechanism) can improve a concret design, with real-life examples. Starting with a native design leveraging only a few tricks from the typing system up to a final version where constraints are properly encoded.