Changes between Version 4 and Version 5 of TypeFunctions/TotalFamilies


Ignore:
Timestamp:
Apr 6, 2008 10:42:47 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions/TotalFamilies

    v4 v5  
    1717-- meets only the Relaxed Condition 
    1818type family x :* y 
    19 type instance Z     :* y = Z 
    20 type instance (S x) :* y = x :* y :+ y 
     19type instance Z   :* y = Z 
     20type instance S x :* y = x :* y :+ y 
    2121}}} 
    2222The family `(:+)` meets the ''Relaxed Condition'', but not the ''Strong Termination Condition''.  However, `(:*)` meets not even the ''Relaxed Condition''.  Nevertheless, we would expect that families defined by structural recursion should not compromise termination.  Another somewhat irritating aspect of this example is that we would like these definitions to be closed, but they are open in their present form. 
     
    4949 
    5050type x :* y where 
    51   Z     :* y = Z 
    52   (S x) :* y = x :* y :+ y 
     51  Z   :* y = Z 
     52  S x :* y = x :* y :+ y 
    5353}}} 
    5454In 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 
     
    6565We denote the rewrite system for `TypeEq` as 
    6666{{{ 
    67 Et: {TypeEq s s ~ TTrue; TypeEq st ~ TFalse} 
     67Et: {TypeEq s s ~ TTrue; TypeEq s t ~ TFalse} 
    6868}}} 
    6969and that of the type-level addition and multiplication as 
    7070{{{ 
    71 Et: {Z :+ y ~ y; S x :+ y ~ S (x :+ y); _ :+ _ ~ VOID} 
    72       {Z :* y ~ Z; (S x) :* y ~ x :* y :+ y; _ :* _ ~ VOID} 
     71Et: {Z   :+ y ~ y; 
     72     S x :+ y ~ S (x :+ y);  
     73     _   :+ _ ~ VOID} 
     74    {Z   :* y ~ Z;  
     75     S x :* y ~ x :* y :+ y;  
     76     _   :* _ ~ VOID} 
    7377}}} 
     78Matching on such ''rewrite rule blocks'' starts with the first equality.  If a given family application cannot possibly match on the first equality, the second is considered, and so on.  The last one is guaranteed to match, and this is what makes the definitions total.  Consider the following examples: 
     79 * `TypeEq Int Int  -->  TTrue` 
     80 * `TypeEq Int Bool  -->  TFalse` 
     81 * `TypeEq a b` where `a` and `b` are two rigid type variables, can't be rewritten without further information about `a` and `b`. 
    7482 
    7583=== Critical examples from the paper ===