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 calledNiland the otherCons a (List a).- You can directly write
Nilto get a value of typeList a, with typeato 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 ofashould be inferred from the context. But this time it’s often more direct, asais 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?”