← Midwinter Fair 2009 | Transforming polymorphic values →

# GADTs in Haskell 98

Last time we saw how some type classes can be reified to datatypes, transformed in arbitrary ways and then transformed back again to polymorphic types. I briefly mentioned that for some type classes you need GADTs rather than classical ADTs.

The dual to this story holds as well: many (if not all) GADTs can be represented as type classes. To see how, take a look at the standard GADT example:

data Term :: * -> * where Lit :: Int -> Term Int Inc :: Term Int -> Term Int IsZ :: Term Int -> Term Bool If :: Term Bool -> Term a -> Term a -> Term a Pair :: Term a -> Term b -> Term (a,b) Fst :: Term (a,b) -> Term a Snd :: Term (a,b) -> Term b

Each constructor result type is indexed by the type of the construct it represents. This example is explained in detail in Simple Unification-based Type Inference for GADTs by Simon Peyton Jones et al.

Writing `Term`

like this allows the following well-typed evaluation function:

eval :: Term a -> a eval term = case term of Lit n -> n Inc t -> eval t + 1 IsZ t -> eval t == 0 If c x y -> if eval c then eval x else eval y Pair x y -> (eval x, eval y) Fst t -> fst (eval t) Snd t -> snd (eval t)

To convert a GADT `G`

to a type class, create a new type class `GC`

with one type parameter `g`

. This type parameter `g`

will have the same kind as `G`

, and its arguments will have the same semantics as those of the `G`

. Then for each constructor create one function in the type class with the exact same type, replacing every occurrence of `G`

by `g`

.

If we follow this recipe for `Term`

we get:

class TermC term where lit :: Int -> term Int inc :: term Int -> term Int isZ :: term Int -> term Bool if_ :: term Bool -> term a -> term a -> term a pair :: term a -> term b -> term (a, b) fst_ :: term (a, b) -> term a snd_ :: term (a, b) -> term b

I’ve used the same names as the constructors except I made them lowercase. I appended `_`

to some to avoid name clashes (`fst`

, `snd`

) or lexical errors (`if`

).

Of course, the free instance of `TermC`

is `Term`

.

Now the recipe doesn’t make any assumptions about the GADT in question, but I don’t know if this is right, because you can do some powerful things with GADTs. The two special things in datatypes I can think of—class constraints and existentially quantified variables—are no problem in type classes. Also the thing that makes GADTs truly special—custom type indices in constructor result types—have always been allowed in type classes. If I have overlooked something, please let me know and leave a comment.

However, perhaps the more important question is: can we do everything with `TermC`

that we could do with `Term`

? Well, we can certainly implement `eval`

: this becomes a newtype with a corresponding `instance TermC`

:

newtype Eval a = Eval { evalC :: a } instance TermC Eval where lit = Eval inc t = Eval $ evalC t + 1 isZ t = Eval $ evalC t == 0 if_ c x y = Eval $ if evalC c then evalC x else evalC y pair x y = Eval $ (evalC x, evalC y) fst_ t = Eval $ fst (evalC t) snd_ t = Eval $ snd (evalC t)

The instance is very, very similar to the original evaluation function. Only instead of recursively calling `eval`

, we call `evalC`

and wrap the result in an `Eval`

constructor. The type of `evalC :: Eval a -> a`

is also similar to `eval :: Term a -> a`

.

What I like most about encoding terms and their evaluation this way is that all the code is Haskell 98!

But not everything is this easy. The step evaluator on the Haskell wiki page on GADTs, for example, uses deep pattern matching and as we saw last time this is a lot easier to do on datatypes than in class instances. In fact, I don’t know if this particular example is possible to translate at all, and if it is, it’s certainly not going to be Haskell 98.

Another thing GADTs are useful for is witnesses in families of types. Again, I don’t know if it is possible to translate this use case to class instances.

Summing up, any GADT can be translated to a type class, but not all uses of GADTs have obvious translations. The standard GADT example, however, is trivial to translate. For that reason, it is probably not the most interesting choice as standard example of GADTs.

## Comments

What I like about GADTs is not what they let us do, but what they stop us from doing. The standard GADT example you show makes it impossible to produce an ill-typed Term (not term, Term) without using error or naughty recursion. Using the type class TermC, you have to either give up pattern matching or type safety.

Aha, I never realized you could encode GADTs as type classes like this! Simple once you see it. Thanks for sharing!

Jacques Carette and Oleg Kiselyov and I wrote up some more things that one can do (and have been done) in this way: “Finally

tagless, partially evaluated: Tagless staged interpreters for simpler

typed languages.” Journal of Functional Programming 19(5):509-543.

Unfortunately, not all GADTs can be expressed faithfully in this way, due to “leakage” between the types used for representation and the type parameters in the constructors. An example is given in Section 4 of the paper “Unembedding domain-specific languages” (available from my home page), where we called them “exotically typed terms”. The example in the paper involves Higher-Order Abstract Syntax, but it still happens when you have no negative occurrences of the type variable: a simple example is a GADT for representing typed S and K combinators with application. The problem seems to occur when there is a type parameter inside a GADT term that does not appear on the outside of the term.

Fortunately, all is not lost (if you allow yourself Haskell98 + Rank-2 polymorphism + existential types). One can still represent the Equality GADT as a type class (with single method refl :: f a a), and then use Neil Ghani and Patty Johann’s decomposition of GADTs into normal algebraic datatypes plus the equality GADT. Oleg did this in OCaml in a post to the OCaml mailing list. A disadvantage of this approach is that you have to apply the type equalities by hand.

## Leave a comment!

Martijn loves to receive comments! Add yours by filling out the fields below.