Changes between Version 59 and Version 60 of TypeFunctionsSolving

Aug 17, 2008 3:15:00 PM (7 years ago)



  • TypeFunctionsSolving

    v59 v60  
    136136Propagation 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 (`&`). 
     138Below 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. 
    138140=== Rules === 
    170172where `x` occurs in `F`.  (`co1` may be local or wanted.) 
    172 === Rule application === 
     174=== Rule application: specification === 
     176Propagation 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: 
     178Propagate = fix (Top | SubstFam | SubstVarVar | SubstVarFam) 
     181=== Rule application: algorithm === 
    174183The following function gets a list with all local and wanted equalities.  It returns a list of residual equalities that permit no further rule application. 
    176 {{{ 
     185-- all four rule functions return Nothing if rule not applicable 
     186applyTop         :: RewriteInst -> Maybe EqInst 
     187applySubstFam    :: RewriteInst -> RewriteInst -> Maybe EqInst    -- return only... 
     188applySubstVarVar :: RewriteInst -> RewriteInst -> Maybe EqInst    -- ...the modified... 
     189applySubstVarFam :: RewriteInst -> RewriteInst -> Maybe EqInst    -- ...equality 
    177191propagate :: [RewriteInst] -> [RewriteInst] 
    178192propagate eqs = snd (prop eqs []) 
    182196    prop (eq:eqs) res = apply eq eqs res 
    184     apply [[co :: F ~ t]] eqs res = ...apply (Top) to lhs exhaustively, then try pairwise rules 
    185 }}} 
    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 non-termination.  (It seems we can drop this requirement if we only ever substitute into left-hand sides.) 
    192  * We should probably use !SubstVar on all variable equalities before using !SubstFam, as the former may refine the left-hand 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 left-hand 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 left-hand sides (not in right-hand 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 left-hand sides? 
    196 Notes: 
    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 ~ t]] eqs res  
     199      | Just eq' <- applyTop eq = prop (norm eq' ++ eqs) res 
     200      | otherwise        = mapRule (applySubstFam eq) -- TODO!!! 
    200203=== Observations === 
    202205 * Only !SubstVarFam when replacing a variable in a family equality can  lead to recursion with (Top). 
    203206 * A significant difference to `new-single` 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 right-hand sides anymore.  Moreover, in the concrete implementation, variables may also be re-introduced due to simplification of type classes (which currently doesn't happen in the same iteration). 
    212216 * (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 new-single.) 
    213217* '''TODO:''' Now that we delay instantiation until after solving, do we still need to prioritise flexible variables equalities over rigid ones?  (Probably not.) 
     221'''TODO:'''  Still need to adapt example to new rule set!