Changes between Version 2 and Version 3 of TypeFunctions/TotalFamilies


Ignore:
Timestamp:
Apr 6, 2008 9:54:31 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions/TotalFamilies

    v2 v3  
    3131}}} 
    3232Unfortunately, the two instances are overlapping and there is no means by which we can disambiguate the overlap by using the same textual ordering as that which we are used to from value-level functions. 
     33 
     34=== Defining total families === 
     35 
     36To enable textual disambiguation of overlapping instances, we declare the equalities together (by transferring GADT syntax to type synonyms): 
     37{{{ 
     38type TypeEq s t where 
     39  TypeEq s s = TTrue 
     40  TypeEq s t = TFalse 
     41}}} 
     42`TypeEq` is a standard type family, but by virtue of being total (i.e., exhaustive) it is also closed.  Further equalities cannot define it any further. 
     43 
     44Let's use the same idea for the addition/multiplication examples: 
     45{{{ 
     46type x :+ y where 
     47  Z   :+ y = y 
     48  S x :+ y = S (x :+ y) 
     49 
     50type x :* y where 
     51  Z     :* y = Z 
     52  (S x) :* y = x :* y :+ y 
     53}}} 
     54In contrast to `TypeEq`, `(:+)` and `(:*)` is not total without an extra equality.  We take another idea from value-level function definitions and implicitly complete each of these definitions by a final catch all equality.  So, for `(:+)`, we assume a final 
     55{{{ 
     56x :+ y = VOID 
     57}}} 
     58and for `(:*)` a final 
     59{{{ 
     60x :* y = VOID 
     61}}} 
     62 
     63=== Critical examples from the paper === 
     64 
     65