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
Niland the other
Cons a (List a).
- You can directly write
Nilto get a value of type
List a, with type
ato 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
ashould be inferred from the context. But this time it’s often more direct, as
ais 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
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
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
Added. 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
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)
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.
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)
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)
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
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
This is the so called “type witness”. But how can this be used? (to be continued)