**25**

**1**

**1**

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.

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

**25**

**1**

**1**