Changes between Version 59 and Version 60 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 17, 2008 3:15:00 PM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • 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 (`&`). 
    137137 
     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. 
     139 
    138140=== Rules === 
    139141 
     
    170172where `x` occurs in `F s1..sn`.  (`co1` may be local or wanted.) 
    171173 
    172 === Rule application === 
     174=== Rule application: specification === 
     175 
     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: 
     177{{{ 
     178Propagate = fix (Top | SubstFam | SubstVarVar | SubstVarFam) 
     179}}} 
     180 
     181=== Rule application: algorithm === 
    173182 
    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. 
    175  
    176 {{{ 
     184{{{ 
     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 
     190 
    177191propagate :: [RewriteInst] -> [RewriteInst] 
    178192propagate eqs = snd (prop eqs []) 
     
    182196    prop (eq:eqs) res = apply eq eqs res 
    183197 
    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 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? 
    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}}} 
    199202 
    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). 
    204208 
    205209 
     
    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.) 
     218 
     219---- 
     220 
     221'''TODO:'''  Still need to adapt example to new rule set! 
    214222 
    215223