View source for GADTs for dummies

[[Category:Tutorials]]
[[Category:Language extensions]]

For a long time, I didn't understand what [[Generalised algebraic datatype]]s were or how they could be used. It almost seemed a conspiracy of silence &mdash; people who understood GADTs thought
that everything was obvious and didn't need further explanation, but I still
couldn't understand them.

Now that I have an idea of how it works, I think that it was really obvious. :)  So, I want to share my understanding of GADTs. Maybe the way I realized how GADTs work could help
someone else. 

There are plenty of GADT-related papers, but the best one for beginners
is [http://www.cs.ox.ac.uk/ralf.hinze/publications/With.pdf "Fun with phantom types"].
Phantom types is another name of GADT. You should also know that this
paper uses old GADT syntax. This paper is a must-read because it
contains several examples of practical GADT usage - a theme completely
omitted from this article. For example, the paper outlines how to do binary compression
on datatypes without using typeclasses,
and suggests how to make a kind of printf function.

== Type functions ==

A <hask>data</hask> declaration is a way to declare both type constructor and data
constructors. For example,

<haskell>
data Either a b = Left a | Right b
</haskell>

declares type constructor <hask>Either</hask> and two data constructors <hask>Left</hask>
and <hask>Right</hask>. Ordinary Haskell functions work with data constructors:

<haskell>
isLeft :: Either a b -> Bool
isLeft (Left _) = True
isLeft (Right _) = False
</haskell>

but there is also an analogous way to work with type constructors!

<haskell>
type X a = Either a a
</haskell>

declares a TYPE FUNCTION named <hask>X</hask>. Its parameter <hask>a</hask> must be some type
and it returns some type as its result. We can't use <hask>X</hask> on data values,
but we can use it on type values. Type constructors declared with
<hask>data</hask> statements and type functions declared with <hask>type</hask> statements
can be used together to build arbitrarily complex types. In such
"computations" type constructors serves as basic "values" and type
functions as a way to process them.

Indeed, type functions in Haskell are very limited compared to
ordinary functions - they don't support pattern matching,
nor multiple statements, nor recursion.

== Hypothetical Haskell extension - Full-featured type functions ==

Let's build a hypothetical Haskell extension that mimics, for type
functions, the well-known ways to define ordinary functions, including
pattern matching:

<haskell>
type F [a] = Set a
</haskell>

multiple statements (this is meaningful only in the presence of pattern matching):

<haskell>
type F Bool   = Char
     F String = Int
</haskell>

and recursion (which again needs pattern matching and multiple statements):

<haskell>
type F [a]       = F a
     F (Map a b) = F b
     F (Set a)   = F a
     F a         = a
</haskell>

As you may already have guessed, this last definition calculates a simple base type of arbitrarily-nested collections, e.g.: 

<haskell>
F [[[Set Int]]] = 
F [[Set Int]] =
F [Set Int] = 
F (Set Int) =
F Int =
Int
</haskell>

Let's not forget about statement guards:

<haskell>
type F a | IsSimple a == TrueType  = a
</haskell>

Here we define type function F only for simple datatypes by using a
guard type function "IsSimple":

<haskell>
type IsSimple Bool = TrueType
     IsSimple Int = TrueType
     ....
     IsSimple Double = TrueType
     IsSimple a = FalseType

data TrueType = T
data FalseType = F
</haskell>

These definitions seem a bit odd, and while we are in imaginary land,
let's consider a way to write this shorter:

<haskell>
type F a | IsSimple a  = a

type IsSimple Bool
     IsSimple Int
     ....
     IsSimple Double
</haskell>

Here, we defined a list of simple types. The implied result of all
written statements for "IsSimple" is True, and False for
everything else. Essentially, "IsSimple" is a TYPE PREDICATE!

I really love it! :)  How about constructing a predicate that traverses a
complex type trying to decide whether it contains "Int" anywhere?

<haskell>
type HasInt Int
     HasInt [a] = HasInt a
     HasInt (Set a) = HasInt a
     HasInt (Map a b) | HasInt a
     HasInt (Map a b) | HasInt b
</haskell>

or a type function that substitutes one type with another inside
arbitrarily-deep types:

<haskell>
type Replace t a b | t==a    =  b
     Replace [t] a b         =  [Replace t a b]
     Replace (Set t) a b     =  Set (Replace t a b)
     Replace (Map t1 t2) a b =  Map (Replace t1 a b) (Replace t2 a b)
     Replace t a b           =  t
</haskell>
     
== One more hypothetical extension - multi-value type functions ==

Let's add more fun! We will introduce one more hypothetical Haskell
extension - type functions that may have MULTIPLE VALUES. Say,

<haskell>
type Collection a = [a]
     Collection a = Set a
     Collection a = Map b a
</haskell>

So, "Collection Int" has "[Int]", "Set Int" and "Map String Int" as
its values, i.e. different collection types with elements of type
"Int".

Pay attention to the last statement of the "Collection" definition, where
we used the type variable "b" that was not mentioned on the left side,
nor defined in any other way. Since it's perfectly possible for the
"Collection" function to have multiple values, using some free variable on
the right side that can be replaced with any type is not a problem
at all. "Map Bool Int", "Map [Int] Int" and "Map Int Int" all are
possible values of "Collection Int" along with "[Int]" and "Set Int".

At first glance, it seems that multiple-value functions are meaningless - they
can't be used to define datatypes, because we need concrete types here. But
if we take another look, they can be useful to define type constraints and
type families.

We can also represent a multiple-value function as a predicate:

<haskell>
type Collection a [a]
     Collection a (Set a)
     Collection a (Map b a)
</haskell>

If you're familiar with Prolog, you should know that a predicate, in contrast to
a function, is a multi-directional thing - it can be used to deduce any
parameter from the other ones. For example, in this hypothetical definition:

<haskell>
head | Collection Int a  ::  a -> Int
</haskell>

we define a 'head' function for any Collection containing Ints.

And in this, again, hypothetical definition:

<haskell>
data Safe c  | Collection c a =  Safe c a
</haskell>

we deduced element type 'a' from collection type 'c' passed as the
parameter to the type constructor.



== Back to real Haskell - type classes ==

After reading about all of these glorious examples, you may be wondering
"Why doesn't Haskell support full-featured type functions?" Hold your breath...
Haskell already contains them, and GHC has implemented all of the
capabilities mentioned above for more than 10 years! They were just named...
TYPE CLASSES! Let's translate all of our examples to their language:

<haskell>
class IsSimple a
instance IsSimple Bool
instance IsSimple Int
     ....
instance IsSimple Double
</haskell>

The Haskell'98 standard supports type classes with only one parameter.
That limits us to only defining type predicates like this one. But GHC and
Hugs support multi-parameter type classes that allow us to define
arbitrarily-complex type functions

<haskell>
class Collection a c
instance Collection a [a]
instance Collection a (Set a)
instance Collection a (Map b a)
</haskell>

All of the "hypothetical" Haskell extensions we investigated earlier are
actually implemented at the type class level!

Pattern matching:

<haskell>
instance Collection a [a]
</haskell>

Multiple statements:

<haskell>
instance Collection a [a]
instance Collection a (Set a)
</haskell>

Recursion:

<haskell>
instance (Collection a c) => Collection a [c]
</haskell>

Pattern guards:

<haskell>
instance (IsSimple a) => Collection a (UArray a)
</haskell>



Let's define a type class which contains any collection which uses Int in
its elements or indexes:

<haskell>
class HasInt a
instance HasInt Int
instance (HasInt a) => HasInt [a]
instance (HasInt a) => HasInt (Map a b)
instance (HasInt b) => HasInt (Map a b)
</haskell>


Another example is a class that replaces all occurrences of 'a' with
'b' in type 't' and return the result as 'res':

<haskell>
class Replace t a b res
instance Replace t a a t
instance (Replace t a b res)
          => Replace [t] a b [res]
instance (Replace t a b res)
          => Replace (Set t) a b (Set res)
instance (Replace t1 a b res1, Replace t2 a b res2)
          => Replace (Map t1 t2) a b (Map res1 res2)
instance Replace t a b t
</haskell>

You can compare it to the hypothetical definition we gave earlier.
It's important to note that type class instances, as opposed to
function statements, are not checked in order. Instead, the most
_specific_ instance is automatically selected. So, in the Replace case, the
last instance, which is the most general instance, will be selected only if all the others
fail to match, which is what we want.

In many other cases this automatic selection is not powerful enough
and we are forced to use some artificial tricks or complain to the
language developers. The two most well-known language extensions
proposed to solve such problems are instance priorities, which allow
us to explicitly specify instance selection order, and '/=' constraints,
which can be used to explicitly prohibit unwanted matches:

<haskell>
instance Replace t a a t
instance (a/=b)   => Replace [t] a b [Replace t a b]
instance (a/=b, t/=[_]) => Replace t a b t
</haskell>

You can check that these instances no longer overlap.


In practice, type-level arithmetic by itself is not very useful. It becomes a
fantastic tool when combined with another feature that type classes provide -
member functions. For example:

<haskell>
class Collection a c where
    foldr1 :: (a -> a -> a) -> c -> a
    
class Num a where
    (+) :: a -> a -> a

sum :: (Num a, Collection a c) =>  c -> a
sum = foldr1 (+)
</haskell>


I'll also be glad to see the possibility of using type classes in data
declarations, like this:

<haskell>
data Safe c = (Collection c a) => Safe c a
</haskell>

but as far as I know, this is not yet implemented.


UNIFICATION
...

== Back to GADTs ==

If you are wondering how all of these interesting type manipulations relate to
GADTs, here is the answer. As you know, Haskell contains highly
developed ways to express data-to-data functions. We also know that
Haskell contains rich facilities to write type-to-type functions in the form of
"type" statements and type classes.  But how do "data" statements fit into this
infrastructure?

My answer: they just define a type-to-data constructor translation.  Moreover,
this translation may give multiple results. Say, the following definition:

<haskell>
data Maybe a = Just a | Nothing
</haskell>

defines type-to-data constructors function "Maybe" that has a parameter
"a" and for each "a" has two possible results - "Just a" and
"Nothing". We can rewrite it in the same hypothetical syntax that was
used above for multi-value type functions:

<haskell>
data Maybe a = Just a
     Maybe a = Nothing
</haskell>

Or how about this:

<haskell>
data List a = Cons a (List a)
     List a = Nil
</haskell>

and this:

<haskell>
data Either a b = Left a
     Either a b = Right b
</haskell>

But how flexible are "data" definitions? As you should remember, "type"
definitions were very limited in their features, while type classes,
on the other hand, were more developed than ordinary Haskell functions
facilities. What about features of "data" definitions examined as sort of functions?

On the one hand, they supports multiple statements and multiple results and
can be recursive, like the "List" definition above. On the other, that's all -
no pattern matching or even type constants on the left side and no guards.

Lack of pattern matching means that the left side can contain only free type
variables. That in turn means that the left sides of all "data" statements for a
type will be essentially the same. Therefore, repeated left sides in
multi-statement "data" definitions are omitted and instead of

<haskell>
data Either a b = Left a
     Either a b = Right b
</haskell>

we write just

<haskell>
data Either a b = Left a
                | Right b
</haskell>


And here we finally come to GADTs! It's just a way to define data types using
pattern matching and constants on the left side of "data" statements!
Let's say we want to do this:

<haskell>
data T String = D1 Int
     T Bool   = D2
     T [a]    = D3 (a,a)
</haskell>


We cannot do this using a standard data definition. So, now we must use a GADT definition:

<haskell>
data T a where
    D1 :: Int -> T String
    D2 :: T Bool
    D3 :: (a,a) -> T [a]
</haskell>

Amazed? After all, GADTs seem to be a really simple and obvious extension to
data type definition facilities.







The idea here is to allow a data constructor's return type to be specified
directly:

<haskell>
data Term a where
    Lit :: Int ->  Term Int
    Pair :: Term a -> Term b -> Term (a,b)
    ...
</haskell>

In a function that performs pattern matching on Term, the pattern match gives
type as well as value information. For example, consider this function:

<haskell>
eval :: Term a -> a
eval (Lit i)     = i
eval (Pair a b)  = (eval a, eval b)
...
</haskell>

If the argument matches Lit, it must have been built with a Lit constructor,
so type 'a' must be Int, and hence we can return 'i' (an Int) in the right
hand side. The same thing applies to the Pair constructor.






== Further reading ==

The best paper on type level arithmetic using type classes I've seen
is "Faking it: simulating dependent types in Haskell"
( http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2636 ). Most of
this article comes from his work.

I should also mention here [http://okmij.org/ftp/Haskell/types.html Oleg Kiselyov's page on type-level programming in Haskell].


Other GADT-related papers:

* [http://www.cs.nott.ac.uk/~nhn/Publications/icfp2005.pdf "Dynamic Optimization for Functional Reactive Programming using Generalized Algebraic Data Types"]

* [http://citeseer.ist.psu.edu/rd/0,606209,1,0.25,Download/http:qSqqSqwww.informatik.uni-bonn.deqSq~ralfqSqpublicationsqSqPhantom.ps.gz "Phantom Types"] (actually a more scientific version of "Fun with phantom types")

* [http://arxiv.org/ps/cs.PL/0403034 "Phantom types and subtyping"]

* "Existentially quantified type classes" by Stuckey, Sulzmann and Wazny (URL?)