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?”