Haskell/GADT

From Wikibooks, the open-content textbooks collection

Wikipedia has related information at GADT.

[edit] Introduction

TODO: Explain what a GADT (Generalised Algebraic Datatype) is, and what it's for

TODO:? Generalised Algebraic Datatypes provide two new things: (1) a way to make your datatypes more precise and thus safer and (2) a nice new syntax which also unifies a lot of recent ideas about typing into a uniform presentation

[edit] GADT-style syntax

Before getting into GADT-proper, let's start out by getting used to the new syntax. Here is a representation for the familiar List type in both normal Haskell style and the new GADT one:

data List x =
 Nil  |
 Cons x (List x)

data List x where
 Nil  :: List x
 Cons :: x -> List x -> List x

Up to this point, we have not introduced any new capabilities, just a little new syntax. Strictly speaking, we are not working with GADTs yet, but GADT syntax. The new syntax should be very familiar to you in that it closely resembles typeclass declarations. It should also be easy to remember if you like to think of constructors as just being functions. Each constructor is just defined like a type signature for any old function.

[edit] What GADTs give us

Given a data type Foo a, a constructor for Foo is merely a function that takes some number of arguments and gives you back a Foo a. So what do GADTs add for us? The ability to control exactly what kind of Foo you return. With GADTs, a constructor for Foo a is not obliged to return Foo a; it can return any Foo ??? that you can think of. In the code sample below, for instance, the GadtedFoo constructor returns a GadtedFoo Int even though it is for the type GadtedFoo x.

Example: GADT gives you more control

data BoringFoo x where
 MkBoringFoo :: x -> BoringFoo x

data GadtedFoo x where
 MkGadtedFoo :: x -> GadtedFoo Int

But note that you can only push the idea so far... if your datatype is a Foo, you must return some kind of Foo or another. Returning anything else simply wouldn't work

Example: Try this out. It doesn't work

data Bar where
  MkBar :: Bar -- This is ok

data Foo where
  MkFoo :: Bar -- This is bad

[edit] Safe Lists

Prerequisite: We assume in this section that you know how a List tends to be represented in functional languages

We've now gotten a glimpse of the extra control given to us by the GADT syntax. The only thing new is that you can control exactly what kind of data structure you return. Now, what can we use it for? Consider the humble Haskell list. What happens when you invoke head []? Haskell blows up. Have you ever wished you could have a magical version of head that only accepts lists with at least one element, lists on which it will never blow up?

To begin with, let's define a new type, SafeList x y. The idea is to have something similar to normal Haskell lists [x], but with a little extra information in the type. This extra information (the type variable y) tells us whether or not the list is empty. Empty lists are represented as SafeList x Empty, whereas non-empty lists are represented as SafeList x NonEmpty.

-- we have to define these types
data Empty
data NonEmpty

-- the idea is that you can have either 
--    SafeList x Empty
-- or SafeList x NonEmpty
data SafeList x y where
-- to be implemented

Since we have this extra information, we can now define a function safeHead on only the non-empty lists! Calling safeHead on an empty list would simply refuse to type-check.

safeHead :: SafeList x NonEmpty -> x

So now that we know what we want, safeHead, how do we actually go about getting it? The answer is GADT. The key is that we take advantage of the GADT feature to return two different kinds of lists, SafeList x Empty for the Nil constructor, and SafeList x NonEmpty for the Cons constructors respectively:

data SafeList x y where
  Nil  :: SafeList x Empty
  Cons :: x -> SafeList x y -> SafeList x NonEmpty

This wouldn't have been possible without GADT, because all of our constructors would have been required to return the same type of list; whereas with GADT we can now return different types of lists with different constructors. Anyway, let's put this altogether, along with the actual definition of SafeList:

Example: safe lists via GADT

data Empty
data NonEmpty

data SafeList x y where
     Nil :: SafeList x Empty
     Cons:: x -> SafeList x y  -> SafeList x NonEmpty

safeHead :: SafeList x NonEmpty -> x
safeHead (Cons x _) = x

Copy this listing into a file and load in ghci -fglasgow-exts. You should notice the following difference, calling safeHead on an non-empty and an empty-list respectively:

Example: safeHead is... safe

Prelude Main> safeHead (Cons "hi" Nil)
"hi"
Prelude Main> safeHead Nil

<interactive>:1:9:
    Couldn't match `NonEmpty' against `Empty'
      Expected type: SafeList a NonEmpty
      Inferred type: SafeList a Empty
    In the first argument of `safeHead', namely `Nil'
    In the definition of `it': it = safeHead Nil

This complaint is a good thing: it means that we can now ensure during compile-time if we're calling safeHead on an appropriate list. However, this is a potential pitfall that you'll want to look out for.

Consider the following function. What do you think its type is?

Example: Trouble with GADTs

silly 0 = Nil
silly 1 = Cons 1 Nil

Now try loading the example up in GHCi. You'll notice the following complaint:

Example: Trouble with GADTs - the complaint

Couldn't match `Empty' against `NonEmpty'
     Expected type: SafeList a Empty
     Inferred type: SafeList a NonEmpty
   In the application `Cons 1 Nil'
   In the definition of `silly': silly 1 = Cons 1 Nil

FIXME: insert discussion

[edit] A simple expression evaluator

Insert the example used in Wobbly Types paper... I thought that was quite pedagogical

[edit] Discussion

More examples, thoughts

From FOSDEM 2006, I vaguely recall that there is some relationship between GADT and the below... what?

[edit] Phantom types

See Phantom types.

[edit] Existential types

If you like Existentially quantified types, you'd probably want to notice that they are now subsumbed by GADTs. As the GHC manual says, the following two type declarations give you the same thing.

 data TE a = forall b. MkTE b (b->a)
 data TG a where { MkTG :: b -> (b->a) -> TG a }

Heterogeneous lists are accomplished with GADTs like this:

 data TE2 = forall b. Show b => MkTE2 [b]
 data TG2 where
   MkTG2 :: Show b => [b] -> TG2

[edit] Witness types

[edit] References

This module is a stub. You can help Haskell by expanding it.

At least part of this page was imported from the Haskell wiki article Generalised algebraic datatype, in accordance to its Simple Permissive License. If you wish to modify this page and if your changes will also be useful on that wiki, you might consider modifying that source page instead of this one, as changes from that page may propagate here, but not the other way around. Alternately, you can explicitly dual license your contributions under the Simple Permissive License.