What is GADT (Generalized Algebraic Data Types) in Haskell?

Like
Like Love Haha Wow Sad Angry
3612

We assume that you are familiar with what we are doing without GADT. Say, for the simplest case, we are defining a list:

List a = Nil | Cons a (List a)

What exactly are we doing?

  • On the LHS, it defines a “type constructor” called List. It takes a type as parameter, and returns a new type. It’s essentially a function of types.
  • On the RHS, it tells us that we have two ways to construct a value of type List a. One is called Nil and the other Cons a (List a).
    • You can directly write Nil to get a value of type List a, with type a to be determined, more precisely inferred from the context.
    • In the case of Cons a (List a), it’s actually a function named Cons, taking two parameters, one with type a, the other with type List a. Again, the type of a should be inferred from the context. But this time it’s often more direct, as a is the type of the first parameter.

Then we can represent these two constructors as normal functions: Continue reading “What is GADT (Generalized Algebraic Data Types) in Haskell?”

Like
Like Love Haha Wow Sad Angry
3612