Changes between Version 1 and Version 2 of GADTs


Ignore:
Timestamp:
Dec 1, 2005 7:51:20 PM (8 years ago)
Author:
sweirich@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GADTs

    v1 v2  
    1111    Const :: a -> Term a 
    1212    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 
    1415}}} 
    15 The last two lines also illustrate that these definitions subsume ExistentialQuantification. 
     16The 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. 
    1617 
    17 If the type takes advantage of the generalization, any function that matches on it must be given a signature. 
     18If the type takes advantage of the generalization, any function that matches on it must be given a signature.  
     19 
     20However, 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{{{ 
     22eval :: Term a -> a 
     23eval (Const x) = x 
     24eval (Pair t1 t2) = (eval t1, eval t2) 
     25eval (Fst t1) = fst (eval t1) 
     26eval (Snd t1) = snd (eval t1) 
     27}}} 
    1828 
    1929== References == 
     
    2232 
    2333== Pros == 
    24  * makes the types of data constructors clear 
    25  * 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 properties---one (baby) step towards dependently-typed languages 
    2636 
    2737== Cons == 
    2838 * relatively new 
    2939 * even if old-style datatype declarations are removed, that special case remains important, e.g. in saying when function signatures are required. 
     40 * complex interactions with type classes