Changes between Version 9 and Version 10 of TypeFunctionsSolving
- Timestamp:
- 07/22/08 22:56:29 (5 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
TypeFunctionsSolving
v9 v10 29 29 30 30 * (Unify) is an asymmetric rule, and hence, only fires for equalities of the form `x ~ c`, where `c` is free of synonym families. Moreover, it only applies to wanted equalities. (Rationale: Local equality constraints don't justify global instantiation of flexible type variables.) 31 * (Local) only applies to normalised equalities in Form (2) & (3) - and currently also only to local equalities, not to wanteds. In principle, a rewrite rule could be discarded after an exhaustive application of (Local). However, while the set of class constraints is kept separate, we may always have some occurrences of the supposedly eliminated variable in a class constraint .31 * (Local) only applies to normalised equalities in Form (2) & (3) - and currently also only to local equalities, not to wanteds. In principle, a rewrite rule could be discarded after an exhaustive application of (Local). However, while the set of class constraints is kept separate, we may always have some occurrences of the supposedly eliminated variable in a class constraint, and hence, need to keep all local equalities around. NB: (Local) -for Forms (2) & (3)- is the most expensive rule as it needs to traverse all type terms. 32 32 * (IdenticalLHS) I don't think it is useful to apply that rule when both equalities are wanted, which makes it a variant of (Local). 33 33 34 Observation: 35 * Only (Local) when replacing a variable in the ''left-hand side'' of an equality of Form (1) can lead to recursion with (Top). 34 36 35 37 == Termination == … … 77 79 }}} 78 80 79 Derivation ourmodified rules:81 Derivation with modified rules: 80 82 {{{ 81 83 [F v] ~ v ||- [F v] ~ v
