Changes between Version 5 and Version 6 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 23, 2008 3:38:21 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v5 v6  
    2424 * 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.) 
    2525 
     26 
     27== Solving == 
     28 
     29 * (Unify) is an asymmetric rule, and hence, only fires for equalities of the form `x ~ c`, where `c` is free of synonym families. 
     30 * (Local) only applies to normalised equalities in Form (2) & (3).  After an application of (Local), the rewrite rule can be discarded 
     31 
    2632== Termination == 
    2733 
    28 The Note [skolemOccurs loop] in the old code explains that equalities of the form `x ~ t` (where `x` is a flexible type variable) may not be used as rewrite rules, but only be solved by applying Rule Unify.  As Unify carefully avoids cycles, this prevents the use of equalities introduced by the Rule !SkolemOccurs as rewrite rules.  For this to work, !SkolemOccurs also had to apply to equalities of the form `a ~ t[[a]]`.  This was a somewhat intricate set up that's being simplified in the new algorithm.  Whether equalities of the form `x ~ t` are used as rewrite rules or solved by Unify doesn't matter anymore.  Instead, we disallow recursive equalities completely.  This is possible as right-hand sides are free of synonym families. 
     34=== !SkolemOccurs === 
     35 
     36The Note [skolemOccurs loop] in the old code explains that equalities of the form `x ~ t` (where `x` is a flexible type variable) may not be used as rewrite rules, but only be solved by applying Rule Unify.  As Unify carefully avoids cycles, this prevents the use of equalities introduced by the Rule !SkolemOccurs as rewrite rules.  For this to work, !SkolemOccurs also had to apply to equalities of the form `a ~ t[[a]]`.  This was a somewhat intricate set up that's being simplified in the new algorithm.  Whether equalities of the form `x ~ t` are used as rewrite rules or solved by Unify doesn't matter anymore.  Instead, we disallow recursive equalities after normalisation completely (both locals and wanteds).  This is possible as right-hand sides are free of synonym families. 
     37 
     38To see how the new algorithm handles the type of equalities that required !SkolemOccurs in the ICFP'08 algorithm, consider the following notorious example: 
     39{{{ 
     40E_t: forall x. F [x] ~ [F x] 
     41[F v] ~ v  ||-  [F v] ~ v 
     42}}} 
     43 
     44Derivation with rules in the new-single report: 
     45{{{ 
     46[F v] ~ v  ||-  [F v] ~ v 
     47==> normalise 
     48v ~ [a], F v ~ a  ||-  v ~ [x], F v ~ x 
     49a := F v 
     50==> (Local) with v 
     51F [a] ~ a  ||-  [a] ~ [x], F [a] ~ x 
     52==> normalise 
     53F [a] ~ a  ||-  x ~ a, F[a] ~ x 
     54==> 2x (Top) & Unify 
     55[F a] ~ a  ||-  [F a] ~ a 
     56..and so on.. 
     57}}} 
     58 
     59{{{ 
     60  v ~ [x], F v ~ x 
     61==> (Local) with v 
     62  v ~ [x], F [a] ~ x 
     63==> (Top) 
     64  v ~ [x], x ~ [F x] 
     65===> normalise 
     66  v ~ [x], x ~ [y], F x ~ y 
     67}}}