|Version 1 (modified by ross@…, 11 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) Apply :: Term (a -> b) -> Term a -> Term b
The last two lines also illustrate that these definitions subsume ExistentialQuantification.
If the type takes advantage of the generalization, any function that matches on it must be given a signature.
- GHC Documentation
- Simple unification-based type inference for GADTs by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Submitted to PLDI 2005.
- makes the types of data constructors clear
- permits convenient expression of many properties
- relatively new
- even if old-style datatype declarations are removed, that special case remains important, e.g. in saying when function signatures are required.