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 calledNil
and the otherCons a (List a)
.- You can directly write
Nil
to get a value of typeList a
, with typea
to be determined, more precisely inferred from the context. - In the case of
Cons a (List a)
, it’s actually a function namedCons
, taking two parameters, one with typea
, the other with typeList a
. Again, the type ofa
should be inferred from the context. But this time it’s often more direct, asa
is the type of the first parameter.
- You can directly write
Then we can represent these two constructors as normal functions: Continue reading “What is GADT (Generalized Algebraic Data Types) in Haskell?”