Changes between Version 1 and Version 2 of TypeFunctions/TotalFamilies
 Timestamp:
 Apr 6, 2008 9:31:19 AM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctions/TotalFamilies
v1 v2 5 5 To guarantee the termination and completeness of the solving of equality constraints, we need to impose rather draconian restrictions on the instances of type synonym families. More specifically, to achieve both termination and completeness, we need the ''Strong Termination Condition'' and if we settle for termination alone (accepting to be incomplete for some rather exotic programs), we need the ''Relaxed (Termination) Condition'' as defined in [http://www.cse.unsw.edu.au/~chak/papers/tctfs.pdf Type Checking with Open Type Functions]. The ''Strong Termination Condition'' corresponds closely to the conditions imposed on functional dependencies. The ''Relaxed Condition'' is somewhat more liberal, but still does not permit, for example, nested applications of type families in the righthand side of a `type instance`. For many practically attractive uses of type families, where the the system is actually terminating, this is still to restrictive. 6 6 7 === An example===7 === Two examples === 8 8 9 9 {{{ 10 10 data Z; data S a; 11 11 12  meets the Strong Termination Condition 12 13 type family x :+ y 13 14 type instance Z :+ y = y 14 15 type instance S x :+ y = S (x :+ y) 15 16 17  meets only the Relaxed Condition 16 18 type family x :* y 17 19 type instance Z :* y = Z 18 20 type instance (S x) :* y = x :* y :+ y 19 21 }}} 20 The family `(:+)` meets the ''Relaxed Condition'', but not the ''Strong Termination Condition''. However, `(:*)` meets not even the ''Relaxed Condition''. 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. 23 24 We might want to define equality on types as 25 {{{ 26 data TFalse; data TTrue; 27 28 type family TypeEq s t 29 type instance TypeEq s s = TTrue 30 type instance TypeEq s t = FFalse  matches only if the previous instance does not 31 }}} 32 Unfortunately, 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 valuelevel functions.