Changes between Version 1 and Version 2 of GADTs
 Timestamp:
 Dec 1, 2005 7:51:20 PM (11 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

GADTs
v1 v2 11 11 Const :: a > Term a 12 12 Pair :: Term a > Term b > Term (a,b) 13 Apply :: Term (a > b) > Term a > Term b 13 Fst :: Term (a,b) > Term a 14 Snd :: Term (a,b) > Term b 14 15 }}} 15 The last two lines also illustrate that these definitions subsume ExistentialQuantification .16 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. 16 17 17 If the type takes advantage of the generalization, any function that matches on it must be given a signature. 18 If the type takes advantage of the generalization, any function that matches on it must be given a signature. 19 20 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. 21 {{{ 22 eval :: Term a > a 23 eval (Const x) = x 24 eval (Pair t1 t2) = (eval t1, eval t2) 25 eval (Fst t1) = fst (eval t1) 26 eval (Snd t1) = snd (eval t1) 27 }}} 18 28 19 29 == References == … … 22 32 23 33 == Pros == 24 * makes the types of data constructors clear25 * permits convenient expression of many properties 34 * New syntax for datatypes makes the types of data constructors clear, though may be adopted independently from GADTs. (Convenient for ExistentialQuantification) 35 * permits convenient expression of many propertiesone (baby) step towards dependentlytyped languages 26 36 27 37 == Cons == 28 38 * relatively new 29 39 * even if oldstyle datatype declarations are removed, that special case remains important, e.g. in saying when function signatures are required. 40 * complex interactions with type classes