Changes between Version 4 and Version 5 of TypeFunctions/TotalFamilies
 Timestamp:
 Apr 6, 2008 10:42:47 AM (7 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctions/TotalFamilies
v4 v5 17 17  meets only the Relaxed Condition 18 18 type family x :* y 19 type instance Z 20 type instance (S x):* y = x :* y :+ y19 type instance Z :* y = Z 20 type instance S x :* y = x :* y :+ y 21 21 }}} 22 22 The 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. … … 49 49 50 50 type x :* y where 51 Z 52 (S x):* y = x :* y :+ y51 Z :* y = Z 52 S x :* y = x :* y :+ y 53 53 }}} 54 54 In contrast to `TypeEq`, `(:+)` and `(:*)` is not total without an extra equality. We take another idea from valuelevel function definitions and implicitly complete each of these definitions by a final catch all equality. So, for `(:+)`, we assume a final … … 65 65 We denote the rewrite system for `TypeEq` as 66 66 {{{ 67 Et: {TypeEq s s ~ TTrue; TypeEq s t ~ TFalse}67 Et: {TypeEq s s ~ TTrue; TypeEq s t ~ TFalse} 68 68 }}} 69 69 and that of the typelevel addition and multiplication as 70 70 {{{ 71 Et: {Z :+ y ~ y; S x :+ y ~ S (x :+ y); _ :+ _ ~ VOID} 72 {Z :* y ~ Z; (S x) :* y ~ x :* y :+ y; _ :* _ ~ VOID} 71 Et: {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} 73 77 }}} 78 Matching 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`. 74 82 75 83 === Critical examples from the paper ===