Changes between Version 58 and Version 59 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 17, 2008 11:48:44 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v58 v59  
    9393    (t', eqt) = flatten t 
    9494 
    95 check :: FlattenedEqInst -> [FlattenedEqInst] 
     95check :: FlatEqInst -> [RewriteInst] 
    9696-- Does OccursCheck + Decomp + Triv + Swap (of new-single) 
    9797check [[co :: t ~ t]] = [] with co = id 
     
    109109check [[co :: T ~ S]] = fail 
    110110 
    111 flatten :: Type -> (Type, [FlattenedEqInst]) 
     111flatten :: Type -> (Type, [RewriteInst]) 
    112112-- Result type has no synonym families whatsoever 
    113113flatten [[F t1..tn]] = (alpha, [[id :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn) 
     
    134134== Propagation (aka Solving) == 
    135135 
    136 A significant difference to `new-single` is that solving is a purely local operation.  We never instantiate any flexible variables. 
     136Propagation 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 (`&`). 
    137137 
    138138=== Rules === 
     
    157157{{{ 
    158158co1 :: x ~ t  &  co2 :: x ~ s 
    159 =(SubstVar)=> 
     159=(SubstVarVar)=> 
    160160co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2' 
    161161}}} 
     
    164164 '''!SubstVarFam''':: 
    165165{{{ 
    166 }}} 
     166co1 :: x ~ t  &  co2 :: F s1..sn ~ s 
     167=(SubstVarFam)=> 
     168co1 :: x ~ t  &  co2' :: [t/x](F s1..sn) ~ s with co2 = [co1/x](F s1..sn) |> co2' 
     169}}} 
     170where `x` occurs in `F s1..sn`.  (`co1` may be local or wanted.) 
     171 
     172=== Rule application === 
     173 
     174The 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{{{ 
     177propagate :: [RewriteInst] -> [RewriteInst] 
     178propagate 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 
    167187 
    168188'''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 non-termination.  More precisely, if we interleave Top and !SubstFam, we can easily diverge. 
    173189 * Rules applying to variable equalities: 
    174190  * !SubstVar (formerly, Local) applies to variable equalities (both locals and wanteds) 
     
    184200=== Observations === 
    185201 
    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 `new-single` is that solving is a purely local operation.  We never instantiate any flexible variables. 
    188204 
    189205