**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:

Nil :: List a Cons :: a -> List a -> List a

We can see that they are functions both with the same return type `List a`

. *The only thing that GADT does*, is allowing a specific `a`

here. For example, we can have a constructor with `a`

specifically set to `Int`

, meaning it only constructs values of type `List Int`

.

IntNil :: List Int

We can experiment with some code in the GADT flavor:

data List a where IntNil :: List Int Nil :: List a Cons :: a -> List a -> List a a :: List Int a = IntNil -- Would raise an error for type incompatibility. -- c_ :: List Char -- c_ = IntNil -- This one is compatible. c :: List Char c = Nil

Certainly, `a`

does not have to be a type as simple as `Int`

. It could be an arbitrary type, even `List a`

or `List (List a)`

with `a`

still unspecified:

data Pair a b where Pair :: a -> b -> Pair a b data List a where IntListNil :: List (List Int) ListNil :: List (List a) IntNil :: List Int Nil :: List a Cons :: a -> List a -> List a -- This one is invalid, since the top-level `Pair` is not `List` -- Bad :: a -> List a -> Pair a (List a)

So what can GADT be used for? What can be additionally done with it? Here are some scenarios as far as I know:

The most famous use case is to embed (the AST of) a language into Haskell. Suppose we have such a simple language of expressions:

data Expr = ILit Int | BLit Bool | Add Expr Expr | Eq Expr Expr

Such a data type definition is sufficient to contain the language, but it also contains expressions beyond the language (that is, invalid expressions). For example, `Bool`

values cannot be `Add`

ed. But this definition does not prevents us from writing:

addBool :: Expr addBool = Add (BLit True) (BLit False)

An attempt to fix this is to record the “return type” of an `Expr`

somewhere. Remember we have done that with `List a`

, where we record the member type `a`

in the list type `List a`

. We can do the same to `Expr`

:

data Expr a = ILit Int | BLit Bool | Add (Expr Int) (Expr Int) | Eq (Expr a) (Expr a)

This looks plausible. But there are still problems!

The crucial part is, while `BLit True`

should be `Expr Bool`

so that it cannot be the parameters of `Add`

, it isn’t actually. The `BLit True`

here is still of type `Expr a`

with `a`

undetermined (to be inferred). This is parallel to the case where `Nil`

is of type `List a`

with `a`

undetermined. There is actually no relation between the type of the parameter of the constructor `BLit`

and the type of the constructed value.

Here GADT comes into the play. We can constraint the return type of the constructor only with GADT:

data Expr a where ILit :: Int -> Expr Int BLit :: Bool -> Expr Bool Add :: Expr Int -> Expr Int -> Expr Int -- In the case of Eq, we can loosen the type specification into a typeclass. Eq :: Eq a => Expr a -> Expr a -> Expr Bool

This would achieve the goal:

-- Won't compile, since `BLit True` and `BLit False` are of type `Expr Bool` -- addBool = Add (BLit True) (BLit False) addInt = Add (ILit 1) (ILit 2) eqBool = Eq (BLit True) (BLit False)

Fantastic!

This is the so-called “initial embedding” of a language. The final version we achieved with GADT is a “tagless initial embedding”. Why tagless? Because ADT is the so-called “tagged union”, and we are abandoning it, thus tagless.

The `Expr`

represents a very simple language. You can well embed more complex languages such as simply type lambda calculus.

Contrary to “initial embedding”, there’s “final embedding” as well. But that’s another story.

We can even impose more restrictions on the embed of languages. Suppose we have a language describing stack operations. `Push`

means push a number to the top of the stack. `Add`

means pop the top two numbers and push back their sum:

data StackLang where Begin :: StackLang Push :: Int -> StackLang -> StackLang Add :: StackLang -> StackLang bug = Add (Push 1 Begin)

The `bug`

line reflects a bug that would happen. When there’s only one element in the stack, an `Add`

could not be performed. If only we could eliminate such silly bugs on the type level!

This could be possible when the number of elements in the stack is encoded in the type `StackLang`

. This is exactly where GADT shines:

data Z data S n data SStackLang t where SBegin :: SStackLang Z SPush :: Int -> SStackLang t -> SStackLang (S t) SAdd :: SStackLang (S (S t)) -> SStackLang (S t)

The `Z`

(for 0) and `S`

(for *successor*) here are simulations of the Peano system of natural numbers. Now compiling the following

sBug = SAdd (SPush 1 SBegin)

would raise an error:

• Couldn’t match type ‘Z’ with ‘S t’

Expected type: SStackLang (S (S t))

Actual type: SStackLang (S Z)

Safe as expected.

This is actually a simulation of the *dependent type*. You can define types representing “lists of length n” and so on in this way.

GADT can also convert types into values. You can do this without GADT:

data Witness a = Witness a

But you need to supply a value of type `a`

. What if you cannot find such a value? It’s not reasonable to require a value to encode a type, as such a value may not exist at all! (consider `Void`

)

You can drop this requirement with GADT:

data Witness a where IntWitness :: Witness Int BoollWitness :: Witness Bool

In this way, you directly get a value in the encoded type `Witness a`

, even if there’s no value of the original type `a`

.

This is the so called “type witness”. But how can this be used? (to be continued)

**25**

**1**

**1**

待续

我想念你，诚挚地。