Generalized Abstract Data Types

See ExtensionDescriptionHowto for information on how to write these extension descriptions. Please add any new extensions to the list of HaskellExtensions.

Brief Explanation

An alternative syntax for datatypes, giving explicit type signatures for data constructors, generalized by allowing the arguments of the result type to vary, e.g.

data Term :: * -> * where
    Const :: a -> Term a
    Pair  :: Term a -> Term b -> Term (a,b)
    Fst :: Term (a,b) -> Term a
    Snd :: Term (a,b) -> Term b

The last two lines also illustrate that these definitions subsume ExistentialQuantification, because a type that appears in the argument type of the constructor doesn't appear in the result type of the constructor.

If the type takes advantage of the generalization, any function that matches on it must be given a signature.

However, more specific result types for constructors allows type refinement in pattern matching. For example, in the second branch, we know that a is a pair type, so it is correct to return a pair for that branch.

eval :: Term a -> a
eval (Const x) = x
eval (Pair t1 t2) = (eval t1, eval t2)
eval (Fst t1) = fst (eval t1)
eval (Snd t1) = snd (eval t1)

References

GHC Documentation
Simple unification-based type inference for GADTs by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Submitted to PLDI 2005.

Tickets

#37	add GADTs

Pros

New syntax for datatypes makes the types of data constructors clear, though may be adopted independently from GADTs. (Convenient for ExistentialQuantification)
permits convenient expression of many properties—-one (baby) step towards dependently-typed languages

Cons

relatively new
even if old-style datatype declarations are removed, that special case remains important, e.g. in saying when function signatures are required.
complex interactions with type classes

GADTs