|Version 2 (modified by sweirich@…, 9 years ago) (diff)|
Generalized Abstract Data Types
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)
- GHC Documentation
- Simple unification-based type inference for GADTs by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Submitted to PLDI 2005.
- 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
- 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