Changes between Version 25 and Version 26 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 3, 2008 9:07:21 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v25 v26  
    5858== Normalisation == 
    5959 
    60 (Ignoring the coercions for the moment.) 
    61  
    62 '''SLPJ''': added comments/invariants below, pls check. 
    63  
    64 {{{ 
    65 --    EqInst             Arbitrary equalities 
    66 --    FlattenedEqInst    Any type function application is at the top 
    67 --    RewriteInst        Satisfies invariants above 
     60The following function `norm` turns an arbitrary equality into a set of normal equalities.  (It ignores the coercions for the moment.) 
     61{{{ 
     62data EqInst         -- arbitrary equalities 
     63data FlatEqInst     -- synonym families may only occur outermost on the lhs 
     64data RewriteInst    -- normal equality 
    6865 
    6966norm :: EqInst -> [RewriteInst] 
     
    8178 
    8279check :: FlattenedEqInst -> [FlattenedEqInst] 
    83 -- Does OccursCheck + Decomp + Swap 
     80-- Does OccursCheck + Decomp + Swap (of new-single) 
    8481check [[t ~ t]] = [] 
    8582check [[x ~ t]] | x `occursIn` t = fail 
     
    9592 
    9693flatten :: Type -> (Type, [FlattenedEqInst]) 
    97 -- Result type has no type functions whatsoever 
     94-- Result type has no synonym families whatsoever 
    9895flatten [[F t1..tn]] = (x, [[F t1'..tn' ~ x]] : eqt1++..++eqtn) 
    9996  where 
     
    114111 * Whenever an equality of Form (2) or (3) would be recursive, the program can be rejected on the basis of a failed occurs check.  (Immediate rejection is always justified, as right-hand sides do not contain synonym familles; hence, any recursive occurrences of a left-hand side imply that the equality is unsatisfiable.) 
    115112 * Use flexible tyvars for flattening of locals, too.  (We have flexibles in locals anyway and don't use (Unify) on locals, so the flexibles shouldn't cause any harm, but the elimination of skolems is much easier for flexibles - we just instantiate them.) 
    116  * Do we need to record a skolem elimination substitution for skolems introduced during flattening for wanteds, too? 
     113 * '''TODO:''' Do we need to record a skolem elimination substitution for skolems introduced during flattening for wanteds, too? 
    117114 
    118115 
    119116== Solving == 
    120117 
    121  * (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.)  '''SLPJ''': right, precisely as in `new-single.tex`. 
    122  
    123  * (Local) only applies to normalised equalities in Form (2) & (3) - and currently also only to local equalities, not to wanteds.  '''SLPJ''' by "applies to" I think you mean that only those forms are considered to substitute.  We must ''perform'' the substitution on all constraints, right?  '''SLPJ''' why does it not apply to wanteds?[[BR]][[BR]]  
    124  In principle, a rewrite rule could be discarded after an exhaustive application of (Local).  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.[[BR]][[BR]] 
    125  NB: (Local) -for Forms (2) & (3)- is the most expensive rule as it needs to traverse all type terms. 
     118 * (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.) 
     119 
     120 * (Local) only substitutes normal variable equalities - and currently also only local equalities, not wanteds.  (We should call this Rule (Subst) again.)  
     121 
     122 In principle, a rewrite rule could be discarded after an exhaustive application of (Local).  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. 
    126123 
    127124 * (IdenticalLHS) I don't think it is useful to apply that rule when both equalities are wanted, which makes it a variant of (Local).  '''SLPJ''' good point: in view of (Local) there's no need for (IdenticalLHS) to deal with a given `a~t`.  So if epsilon1 is 'g', the LHS could be restricted to form `F t1..tn` which would be good (in the paper).[[BR]][[BR]] 
    128125 '''SLPJ''' but why do you say that we don't want IdenticalLHS on wanteds?  What about `F a ~ x1, F a ~ Int`.  Then we could unify the HM variable `x` with `Int`. 
    129126 
    130 Observation: 
     127=== Observations === 
     128 *  Rule (Local) -substituting variable equalities- is the most expensive rule as it needs to traverse all type terms. 
    131129 * Only (Local) when replacing a variable in the ''left-hand side'' of an equality of Form (1) can  lead to recursion with (Top). 
    132130