Changes between Version 58 and Version 59 of TypeFunctionsSolving
 Timestamp:
 Aug 17, 2008 11:48:44 AM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v58 v59 93 93 (t', eqt) = flatten t 94 94 95 check :: Flat tenedEqInst > [FlattenedEqInst]95 check :: FlatEqInst > [RewriteInst] 96 96  Does OccursCheck + Decomp + Triv + Swap (of newsingle) 97 97 check [[co :: t ~ t]] = [] with co = id … … 109 109 check [[co :: T ~ S]] = fail 110 110 111 flatten :: Type > (Type, [ FlattenedEqInst])111 flatten :: Type > (Type, [RewriteInst]) 112 112  Result type has no synonym families whatsoever 113 113 flatten [[F t1..tn]] = (alpha, [[id :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn) … … 134 134 == Propagation (aka Solving) == 135 135 136 A significant difference to `newsingle` is that solving is a purely local operation. We never instantiate any flexible variables.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 138 === Rules === … … 157 157 {{{ 158 158 co1 :: x ~ t & co2 :: x ~ s 159 =(SubstVar )=>159 =(SubstVarVar)=> 160 160 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 > co2' 161 161 }}} … … 164 164 '''!SubstVarFam''':: 165 165 {{{ 166 }}} 166 co1 :: x ~ t & co2 :: F s1..sn ~ s 167 =(SubstVarFam)=> 168 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s with co2 = [co1/x](F s1..sn) > co2' 169 }}} 170 where `x` occurs in `F s1..sn`. (`co1` may be local or wanted.) 171 172 === Rule application === 173 174 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 {{{ 177 propagate :: [RewriteInst] > [RewriteInst] 178 propagate eqs = snd (prop eqs []) 179 where 180 prop :: [RewriteInst] > [RewriteInst] > [RewriteInst] 181 prop [] res = res 182 prop (eq:eqs) res = apply eq eqs res 183 184 apply [[co :: F t1..tn ~ t]] eqs res = ...apply (Top) to lhs exhaustively, then try pairwise rules 185 }}} 186 167 187 168 188 '''TODO:''' 169 * Rules applying to family equalities:170 * !SubstFam (formerly, IdenticalLHS) only applies to family equalities (both local and wanteds)171 * Top only applies to family equalities (both locals and wanteds)172 We should apply !SubstFam first as it cheaper and potentially reduces the number of applications of Top. On the other hand, for each family equality, we may want to try to reduce it with Top, and if that fails, use it with !SubstFam. (That strategy should lend itself well to an implementation.) But be careful, we need to apply Top exhaustively, to avoid nontermination. More precisely, if we interleave Top and !SubstFam, we can easily diverge.173 189 * Rules applying to variable equalities: 174 190 * !SubstVar (formerly, Local) applies to variable equalities (both locals and wanteds) … … 184 200 === Observations === 185 201 186 * !SubstVar is the most expensive rule as it needs to traverse all type terms.187 * Only !SubstVar when replacing a variable in a family equality can lead to recursion with (Top).202 * Only !SubstVarFam when replacing a variable in a family equality can lead to recursion with (Top). 203 * A significant difference to `newsingle` is that solving is a purely local operation. We never instantiate any flexible variables. 188 204 189 205