With the -fglasgow-exts flag, GHC lets you declare a data type with no constructors. For example:

  data S      -- S :: *
  data T a    -- T :: * -> *

Syntactically, the declaration lacks the "= constrs" part. The type can be parameterised over types of any kind, but if the kind is not * then an explicit kind annotation must be used (see Section 8.8.3, “Explicitly-kinded quantification”).

Such data types have only one value, namely bottom. Nevertheless, they can be useful when defining "phantom types".

GHC allows type constructors, classes, and type variables to be operators, and to be written infix, very much like expressions. More specifically:

Type synonyms are like macros at the type level, but Haskell 98 imposes many rules on individual synonym declarations. With the -XLiberalTypeSynonyms extension, GHC does validity checking on types only after expanding type synonyms. That means that GHC can be very much more liberal about type synonyms than Haskell 98.

GHC currently does kind checking before expanding synonyms (though even that could be changed.)

After expanding type synonyms, GHC does validity checking on types, looking for the following mal-formedness which isn't detected simply by kind checking:

So, for example, this will be rejected:

  type Pr = (# Int, Int #)

  h :: Pr -> Int
  h x = ...

because GHC does not allow unboxed tuples on the left of a function arrow.

The idea of using existential quantification in data type declarations was suggested by Perry, and implemented in Hope+ (Nigel Perry, The Implementation of Practical Functional Programming Languages, PhD Thesis, University of London, 1991). It was later formalised by Laufer and Odersky (Polymorphic type inference and abstract data types, TOPLAS, 16(5), pp1411-1430, 1994). It's been in Lennart Augustsson's hbc Haskell compiler for several years, and proved very useful. Here's the idea. Consider the declaration:

  data Foo = forall a. MkFoo a (a -> Bool)
           | Nil

The data type Foo has two constructors with types:

  MkFoo :: forall a. a -> (a -> Bool) -> Foo
  Nil   :: Foo

Notice that the type variable a in the type of MkFoo does not appear in the data type itself, which is plain Foo. For example, the following expression is fine:

  [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]

Here, (MkFoo 3 even) packages an integer with a function even that maps an integer to Bool; and MkFoo 'c' isUpper packages a character with a compatible function. These two things are each of type Foo and can be put in a list.

What can we do with a value of type Foo?. In particular, what happens when we pattern-match on MkFoo?

  f (MkFoo val fn) = ???

Since all we know about val and fn is that they are compatible, the only (useful) thing we can do with them is to apply fn to val to get a boolean. For example:

  f :: Foo -> Bool
  f (MkFoo val fn) = fn val

What this allows us to do is to package heterogeneous values together with a bunch of functions that manipulate them, and then treat that collection of packages in a uniform manner. You can express quite a bit of object-oriented-like programming this way.

  MkFoo :: (exists a . (a, a -> Bool)) -> Foo

data Baz = forall a. Eq a => Baz1 a a
         | forall b. Show b => Baz2 b (b -> b)

Baz1 :: forall a. Eq a => a -> a -> Baz
Baz2 :: forall b. Show b => b -> (b -> b) -> Baz

  f :: Baz -> String
  f (Baz1 p q) | p == q    = "Yes"
               | otherwise = "No"
  f (Baz2 v fn)            = show (fn v)

data Counter a = forall self. NewCounter
    { _this    :: self
    , _inc     :: self -> self
    , _display :: self -> IO ()
    , tag      :: a
    }

inc :: Counter a -> Counter a
inc (NewCounter x i d t) = NewCounter
    { _this = i x, _inc = i, _display = d, tag = t } 

display :: Counter a -> IO ()
display NewCounter{ _this = x, _display = d } = d x

counterA :: Counter String 
counterA = NewCounter
    { _this = 0, _inc = (1+), _display = print, tag = "A" }

counterB :: Counter String 
counterB = NewCounter
    { _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }

main = do
    display (inc counterA)         -- prints "1"
    display (inc (inc counterB))   -- prints "##"

-- This is invalid; use explicit NewCounter instead for now
setTag :: Counter a -> a -> Counter a
setTag obj t = obj{ tag = t }

GHC allows you to declare an algebraic data type by giving the type signatures of constructors explicitly. For example:

  data Maybe a where
      Nothing :: Maybe a
      Just    :: a -> Maybe a

The form is called a "GADT-style declaration" because Generalised Algebraic Data Types, described in Section 8.4.6, “Generalised Algebraic Data Types (GADTs)”, can only be declared using this form.

Notice that GADT-style syntax generalises existential types (Section 8.4.4, “Existentially quantified data constructors ”). For example, these two declarations are equivalent:

  data Foo = forall a. MkFoo a (a -> Bool)
  data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }

Any data type that can be declared in standard Haskell-98 syntax can also be declared using GADT-style syntax. The choice is largely stylistic, but GADT-style declarations differ in one important respect: they treat class constraints on the data constructors differently. Specifically, if the constructor is given a type-class context, that context is made available by pattern matching. For example:

  data Set a where
    MkSet :: Eq a => [a] -> Set a

  makeSet :: Eq a => [a] -> Set a
  makeSet xs = MkSet (nub xs)

  insert :: a -> Set a -> Set a
  insert a (MkSet as) | a `elem` as = MkSet as
                      | otherwise   = MkSet (a:as)

A use of MkSet as a constructor (e.g. in the definition of makeSet) gives rise to a (Eq a) constraint, as you would expect. The new feature is that pattern-matching on MkSet (as in the definition of insert) makes available an (Eq a) context. In implementation terms, the MkSet constructor has a hidden field that stores the (Eq a) dictionary that is passed to MkSet; so when pattern-matching that dictionary becomes available for the right-hand side of the match. In the example, the equality dictionary is used to satisfy the equality constraint generated by the call to elem, so that the type of insert itself has no Eq constraint.

For example, one possible application is to reify dictionaries:

   data NumInst a where
     MkNumInst :: Num a => NumInst a

   intInst :: NumInst Int
   intInst = MkNumInst

   plus :: NumInst a -> a -> a -> a
   plus MkNumInst p q = p + q

Here, a value of type NumInst a is equivalent to an explicit (Num a) dictionary.

All this applies to constructors declared using the syntax of Section 8.4.4.2, “Existentials and type classes”. For example, the NumInst data type above could equivalently be declared like this:

   data NumInst a 
      = Num a => MkNumInst (NumInst a)

Notice that, unlike the situation when declaring an existential, there is no forall, because the Num constrains the data type's universally quantified type variable a. A constructor may have both universal and existential type variables: for example, the following two declarations are equivalent:

   data T1 a 
	= forall b. (Num a, Eq b) => MkT1 a b
   data T2 a where
	MkT2 :: (Num a, Eq b) => a -> b -> T2 a

All this behaviour contrasts with Haskell 98's peculiar treatment of contexts on a data type declaration (Section 4.2.1 of the Haskell 98 Report). In Haskell 98 the definition

  data Eq a => Set' a = MkSet' [a]

gives MkSet' the same type as MkSet above. But instead of making available an (Eq a) constraint, pattern-matching on MkSet' requires an (Eq a) constraint! GHC faithfully implements this behaviour, odd though it is. But for GADT-style declarations, GHC's behaviour is much more useful, as well as much more intuitive.

The rest of this section gives further details about GADT-style data type declarations.

Generalised Algebraic Data Types generalise ordinary algebraic data types by allowing constructors to have richer return types. Here is an 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 data types. This generality allows us to 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 t)   = eval t == 0
  eval (If b e1 e2) = if eval b then eval e1 else eval e2
  eval (Pair e1 e2) = (eval e1, eval e2)

The key point about GADTs is that 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 the design closely follows that described in the paper Simple unification-based type inference for GADTs, (ICFP 2006). 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.

These and many other examples are given in papers by Hongwei Xi, and Tim Sheard. There is a longer introduction on the wiki, and Ralf Hinze's Fun with phantom types also has a number of examples. Note that papers may use different notation to that implemented in GHC.

The rest of this section outlines the extensions to GHC that support GADTs. The extension is enabled with -XGADTs. The -XGADTs flag also sets -XRelaxedPolyRec.