Changes between Version 59 and Version 60 of TypeFunctionsSolving
 Timestamp:
 Aug 17, 2008 3:15:00 PM (7 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v59 v60 136 136 Propagation is based on four rules that transform family and variable equalities. The first rule transforms a family equality using a toplevel equality schema. The other three use one equality to transform another. In the presentation, the transforming equality is always first and the transformed is second, separate by an ampersand (`&`). 137 137 138 Below the rules are two scheme for applying the rules. The first one naively iterates until the system doesn't change anymore. The second scheme optimises the iteration somewhat. 139 138 140 === Rules === 139 141 … … 170 172 where `x` occurs in `F s1..sn`. (`co1` may be local or wanted.) 171 173 172 === Rule application === 174 === Rule application: specification === 175 176 Propagation proceeds by applying any of the four rules until the system does not change anymore. After application of a rule, the equalities that were modified need to be normalised again: 177 {{{ 178 Propagate = fix (Top  SubstFam  SubstVarVar  SubstVarFam) 179 }}} 180 181 === Rule application: algorithm === 173 182 174 183 The following function gets a list with all local and wanted equalities. It returns a list of residual equalities that permit no further rule application. 175 176 {{{ 184 {{{ 185  all four rule functions return Nothing if rule not applicable 186 applyTop :: RewriteInst > Maybe EqInst 187 applySubstFam :: RewriteInst > RewriteInst > Maybe EqInst  return only... 188 applySubstVarVar :: RewriteInst > RewriteInst > Maybe EqInst  ...the modified... 189 applySubstVarFam :: RewriteInst > RewriteInst > Maybe EqInst  ...equality 190 177 191 propagate :: [RewriteInst] > [RewriteInst] 178 192 propagate eqs = snd (prop eqs []) … … 182 196 prop (eq:eqs) res = apply eq eqs res 183 197 184 apply [[co :: F t1..tn ~ t]] eqs res = ...apply (Top) to lhs exhaustively, then try pairwise rules 185 }}} 186 187 188 '''TODO:''' 189 * Rules applying to variable equalities: 190 * !SubstVar (formerly, Local) applies to variable equalities (both locals and wanteds) 191 * With !SubstFam and !SubstVar, we always substitute locals into wanteds and never the other way around. We perform substitutions exhaustively. For !SubstVar, this is crucial to avoid nontermination. (It seems we can drop this requirement if we only ever substitute into lefthand sides.) 192 * We should probably use !SubstVar on all variable equalities before using !SubstFam, as the former may refine the lefthand sides of family equalities, and hence, lead to Top being applicable where it wasn't before. 193 * We use !SubstFam and !SubstVar to substitute wanted equalities '''only''' if their lefthand side contains a flexible type variables (which for variable equalities means that we apply !SubstVar only to flexible variable equalities). '''TODO:''' This is not sufficient while we are inferring a type signature as SPJ's example shows: ` a ~ [x], a ~ [Int]`. Here we want to infer `x := Int` before yielding `a ~ [Int]` as an irred. So, we need to use !SubstVar and !SubstFam also if the rhs of a wanted contains a flexible variable. This unfortunately makes termination more complicated. However, SPJ also observed that we really only need to substitute variables in lefthand sides (not in righthand sides) as far as enabling other rewrites goes. However, there are trick problems left as the following two examples show ` a~c, a~b, c~a` and ` b ~ c, b ~ a, a ~ b, c ~ a`. !!Seems SubstVar with a wanted is also sometimes needed if the wanted contains no flexible type variable (as this can trigger applications of Top, which may lead to more specific unifiers). 194 * Substitute only into lefthand sides? 195 196 Notes: 197 198 * In principle, a variable equality could be discarded after an exhaustive application of !SubstVar. 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. That reasoning definitely applies to local equalities, but I think it also applies to wanteds (and I think that GHC so far never applies wanteds to class dictionaries, which might explain some of the failing tests.) Flexible variable equalities cannot be discarded in any case as we need them for finalisation. 198 apply eq@[[co :: F t1..tn ~ t]] eqs res 199  Just eq' < applyTop eq = prop (norm eq' ++ eqs) res 200  otherwise = mapRule (applySubstFam eq)  TODO!!! 201 }}} 199 202 200 203 === Observations === … … 202 205 * Only !SubstVarFam when replacing a variable in a family equality can lead to recursion with (Top). 203 206 * A significant difference to `newsingle` is that solving is a purely local operation. We never instantiate any flexible variables. 207 * We cannot discard any variable equalities after substitution since we do not substitute into righthand sides anymore. Moreover, in the concrete implementation, variables may also be reintroduced due to simplification of type classes (which currently doesn't happen in the same iteration). 204 208 205 209 … … 212 216 * (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  just as in newsingle.) 213 217 * '''TODO:''' Now that we delay instantiation until after solving, do we still need to prioritise flexible variables equalities over rigid ones? (Probably not.) 218 219  220 221 '''TODO:''' Still need to adapt example to new rule set! 214 222 215 223