GADTs for Dummies | Hacker News Reader

GADTs for Dummies

wiki.haskell.org

60 pointsg0xA52A2A30 comments

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

One thing that I'd like to add is that using the typed GADT encoding of the AST lets you write a total eval function such as eval :: AST r → r, no need to return a Maybe or Either! In the case without GADTs you couldn't return a boolean in one case and an Int in another. Here you can.

You know, I did very nearly mention this, but decided not to in the end. You are of course entirely right, and this is indeed a major reason why I use GADTs myself.

Thanks for the amazing explanation.

I tried to implement this in C++ where, as usual, everything is possible but nothing is practical:

https://gcc.godbolt.org/z/9WGxcPWGd

Helpful explanation. I think a lot of the trouble for me in understanding GADTs is the Haskell syntax used in a lot of examples.

My static typing experience is limited to TypeScript and Rust, so I'm curious what a GADT would look like if they were added to those languages.

Here's all the code from the parent in Rusty pseudosyntax:

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

`Not(Equals(Integer(1), Integer(2))) : AST`

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

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

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

`Result(3) : WithError<Int>` `Result(True) : WithError<Bool>`

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

`Weird<String, Bool>` `IgnoreTheType(1) : Weird<String, Bool>` `IgnoreTheType(2) : Weird<Char, Float>` `IgnoreTheType(3) : Weird<Bool, Double>`

`Addition(Boolean(True), Not(Integer(3)))`

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

Finally, we get our GADT:

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

Thanks lalaithion! I don’t know Rust, so it’s interesting to see how different it is compared to Haskell.

A question: how much of this would actually compile in Rust?

- Assuming `Int` and `Bool` are user-defined types (Rust has `bool` and many types of ints like `usize`, `i64`, etc. instead). If you want to work over ANY primitive integer you can use the `num_traits` crate and make your type generic over `num_traits::PrimInt`, or even `num_integer::Integer` to include support for crates such as `num_bigint`.

- Rust needs indirection for recursive data types (like the AST) using `Box`, references, or another kind of indirection. Otherwise, the size isn't known at compile time (since it's potentially infinite).

- Rust doesn't have GADTs (yet?) so the last AST is purely theoretical.

- `IgnoreTheType` (and `AST<R>`) would require explicit use of `PhantomData` for variants without `R` https://doc.rust-lang.org/std/marker/struct.PhantomData.html

On Rust's playground: https://play.rust-lang.org/?version=stable&mode=debug&editio...

Thank you! So it looks like most of my post does indeed work, except for the GADT itself.

(Also, I had not known about Rust Playground, so thanks for introducing me to that too.)

I really like your explanation, which I find easier to understand. I do appreciate your "real-life" AST example, making clear that your are making a better design through the typing system facilities.

Thank you, your explanation was _indeed_ better :-)

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.

Useful take, thanks!

I assume it varies, but I find Idris' dependent type system to be easier to reason about and understand than non-dependent ones I've worked with (say, OCaml and Haskell). Even if Idris can be judged as strictly more powerful in that regard.

There's a sense of a closed loop of consistency and a smaller, tighter set of thought patterns that apply both on this side and the other side – whatever those sides may be, say, values vs. types, compilation vs. runtime, AST vs. raw syntax, parsing vs. printing…

It's an explosion of possibilities!, but as it's a shaped charge of constructive and intuitionistic principles it mostly just blows up shackles and clears the air :)

Yes! I love the consistency of dependent types. You don't need separate declarations for type aliases or a dozen language extensions to do some type-level evaluation, it's quite uniform.

> It's an explosion of possibilities!, but as it's a shaped charge of constructive and intuitionistic principles it mostly just blows up shackles and clears the air :)

Indeed, I feel like we are just getting started finding the right "design patterns" for working with dependently typed programs. It's sort of a Wild West of styles in the Coq world currently, IMO, which is great when something is well designed but terrible when using a theorem demands you prove some clearly obvious precondition (e.g. Riemann integration in the stdlib is a pain to work with).

𝖙𝖍𝖊 𝖔𝖙𝖍𝖊𝖗 𝖘𝖎𝖉𝖊: Having expressibility of Riemann integration near a stdlib at all is marvelous!

I am full pro-Haskell, have used GADTs to define ASTs before and just love length-indexed everything (i.e. nd-matrices) ... but reading your comment I guess somebody who never came in contact with "modern languages" has no idea what you are talking about :-)

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.

OCaml already does. Some good examples -

JSON GADT : https://github.com/OCamlPro/ocplib-json-typed/blob/0d9e9cde7...

Mirage/repr, uses GADT's for representing OCaml types as runtime values which are used for implementing dynamic polymorphism - https://github.com/mirage/repr/blob/main/src/repr/type.ml

I count OCaml as "mainstream" as Haskell ;) it's one of the good ones

Typescript, as a counterexample, doesn't need GADTs because it has first-class union support + nice type filtering. There's a bit of manual tagging that's needed but the ergonomics are both easy to understand and more flexible (not to mention supporting even other usage patterns).

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

Your example doesn't show using a type parameter, which is what makes a GADT a GADT. As far as I can see your example is just an ADT.

Indeed. GADTs provide type equalities and existentials. This example involves neither, only sub-typing (which is quite strong and interesting in Typescript)

Something pretty similar to the AST example in another thread can be implemented in Typescript using sub typing (as it happens, trying to do something like that is how I first found out about GADTs). Looking into existential types, I see that one of the things they can be used for is OOP style subtype polymorphism [1]. Are there things you can do with existential types that can't be done with subtyping?

[1] https://wiki.haskell.org/Existential_type#Dynamic_dispatch_m...

An ADT is a "closed" type like an enum, which then enables other features that you can't implement for OO-style "open" subtyping (e.g. pattern matching). You can encode that in a traditional-OO language with the visitor pattern, but it's very cumbersome to work with in practice.

The other subtle thing with GADTs is that the type information must flow back from the matched case to the type parameter: if you match an Ast<R> and get Mul, you know that R=Int. And that part is impossible to do fully in a language that doesn't have higher-kinded types, because you not only need to be able to know that you can pass an Int where an R was expected, but also that you can pass an Ast<Int> where an Ast<R> is expected, or return a List<Int> where a List<R> is expected, or....

Um that's just an ADT, not a GADT...

Haxe does.

Not that Haxe is mainstream, but it does target mainstream languages.

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.

These are refinement types, rather than dependent types. The main distinction as I understand it being that refinement types allow you to state assertions at a meta-level which are submitted to an SMT solver which may or may not prove them correct, dependent types on the other hand allow expression of arbitrary constraints within the types themselves, along with arbitrary proofs satisfying these types.

Yeah ... I am no expert there. I would guess there is some overlap between refinement and dependent types, thou.

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.

Reply on news.ycombinator.com