Changes between Version 2 and Version 3 of TypeFunctions/TotalFamilies


Ignore:
Timestamp:
Apr 6, 2008 9:54:31 AM (7 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