7.5. Generalised Algebraic Data Types
Prev | Chapter 7. GHC Language Features | Next

## 7.5. Generalised Algebraic Data Types

Generalised Algebraic Data Types (GADTs) generalise ordinary algebraic data types by allowing you to give the type signatures of constructors explicitly. For example:

      data Term a where
          Lit    :: Int -> Term Int
          Succ   :: Term Int -> Term Int
          IsZero :: Term Int -> Term Bool
          If     :: Term Bool -> Term a -> Term a -> Term a
          Pair   :: Term a -> Term b -> Term (a,b)

Notice that the return type of the constructors is not always `Term a`, as is the case with ordinary vanilla data types. Now we can write a well-typed `eval` function for these `Terms`:

      eval :: Term a -> a
      eval (Lit i) 	    = i
      eval (Succ t)     = 1 + eval t
      eval (IsZero i)   = eval i == 0
      eval (If b e1 e2) = if eval b then eval e1 else eval e2
      eval (Pair e1 e2) = (eval e2, eval e2)

These and many other examples are given in papers by Hongwei Xi, and Tim Sheard.

The extensions to GHC are these:

- Data type declarations have a 'where' form, as exemplified above. The type signature of each constructor is independent, and is implicitly universally quantified as usual. Unlike a normal Haskell data type declaration, the type variable(s) in the "`data Term a where`" header have no scope. Indeed, one can write a kind signature instead:

        data Term :: * -> * where ...

  or even a mixture of the two:

        data Foo a :: (* -> *) -> * where ...

  The type variables (if given) may be explicitly kinded, so we could also write the header for `Foo` like this:

        data Foo a (b :: * -> *) where ...

- There are no restrictions on the type of the data constructor, except that the result type must begin with the type constructor being defined. For example, in the `Term` data type above, the type of each constructor must end with `... -> Term ...`.

- You cannot use a `deriving` clause on a GADT-style data type declaration, nor can you use record syntax. (It's not clear what these constructs would mean. For example, the record selectors might ill-typed.) However, you can use strictness annotations, in the obvious places in the constructor type:

        data Term a where
            Lit    :: !Int -> Term Int
            If     :: Term Bool -> !(Term a) -> !(Term a) -> Term a
            Pair   :: Term a -> Term b -> Term (a,b)

- Pattern matching causes type refinement. For example, in the right hand side of the equation

        eval :: Term a -> a
        eval (Lit i) =  ...

  the type `a` is refined to `Int`. (That's the whole point!) A precise specification of the type rules is beyond what this user manual aspires to, but there is a paper about the ideas: "Wobbly types: practical type inference for generalised algebraic data types", on Simon PJ's home page.

  The general principle is this: type refinement is only carried out based on user-supplied type annotations. So if no type signature is supplied for `eval`, no type refinement happens, and lots of obscure error messages will occur. However, the refinement is quite general. For example, if we had:

        eval :: Term a -> a -> a
        eval (Lit i) j =  i+j

  the pattern match causes the type `a` to be refined to `Int` (because of the type of the constructor `Lit`, and that refinement also applies to the type of `j`, and the result type of the `case` expression. Hence the addition `i+j` is legal.

Notice that GADTs generalise existential types. For example, these two declarations are equivalent:

      data T a = forall b. MkT b (b->a)
      data T' a where { MKT :: b -> (b->a) -> T a }

Prev | Up | Next
7.4. Type system extensions | Home | 7.6. Template Haskell