Changes between Version 27 and Version 28 of TypeFunctionsSolving

Timestamp:

08/03/08 02:55:16 (5 years ago)

Author:

chak

Comment:

--

TypeFunctionsSolving

@@ -134 +134 @@
 === !SkolemOccurs ===
 
-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 after normalisation completely (both locals and wanteds).  This is possible as right-hand sides are free of synonym families.
-
-To see how the new algorithm handles the type of equalities that required !SkolemOccurs in the ICFP'08 algorithm, consider the following notorious example:
+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 we seek to simplify here.  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.
+
+To look at this in more detail, let's consider the following notorious example:
 {{{
 E_t: forall x. F [x] ~ [F x]
@@ -142 +142 @@
 }}}
 
-Derivation with rules in the new-single report: 
+'''New-single''': The following derivation shows how the algorithm in new-single fails to terminate for this example.
 {{{
 [F v] ~ v  ||-  [F v] ~ v
@@ -157 +157 @@
 }}}
 
-Same, but de-prioritise (Local) - i.e., (Local) applies only if nothing else does:
+'''New-single using flexible tyvars to flatten locals, but w/o Rule (Local) for flexible type variables''': Interestingly, new-single emulates the effect of (!SkolemOccurs) if we (a) use flexible type variables to flatten local equalities and (b) at the same time do not use Rule (Local) for variable equalities with flexible type variables.  NB: Point (b) was necessary for the ICFP'08 algorithm, too.
+{{{
+[F v] ~ v  ||-  [F v] ~ v
+==> normalise
+v ~ [x2], F v ~ x2  ||-  v ~ [x1], F v ~ x1
+** x2 := F v
+==> (Local) with v
+F [x2] ~ x2  ||-  [x2] ~ [x1], F [x2] ~ x1
+** x2 := F v
+==> normalise
+F [x2] ~ x2  ||-  x2 ~ x1, F [x2] ~ x1
+** x2 := F v
+==> 2x (Top) & Unify
+[F x1] ~ x1  ||-  [F x1] ~ x1
+** x1 := F v
+==> normalise
+x1 ~ [y2], F x1 ~ y2  ||-  x1 ~ [y1], F x1 ~ y1
+** x1 := F v, y2 := F x1
+..we stop here if (Local) doesn't apply to flexible tyvars
+}}}
+A serious disadvantage of this approach is that we '''do''' want to use Rule (Local) with flexible type variables as soon as we have rank-n signatures.  In fact, the lack of doing so is responsible for a few Trac bugs in the GHC implementation of (!SkolemOccurs).
+
+'''De-prioritise Rule (Local)''': Instead of outright forbidding the use of Rule (Local) with flexible type variables, we can simply require that Local is only used if no other rule is applicable.  (That has the same effect on satisfiable queries, and in particular, the present example.)
 {{{
 [F v] ~ v  ||-  [F v] ~ v
@@ -174 +196 @@
 }}}
 
-Same, but de-prioritise (Local) rewriting with equalities of Forms (2) & (3):
+In fact, it is sufficient to de-prioritise Rule (Local) for variable equalities (if it is used for other equalities at all):
 {{{
 [F v] ~ v  ||-  [F v] ~ v
@@ -191 +213 @@
 }}}
 
-Problem is that we still fail to terminate for unsatisfiable queries:
+'''One problems remains''': The algorithm still fails to terminate for unsatisfiable queries.
 {{{
 [F v] ~ v  ||-  [G v] ~ v
@@ -210 +232 @@
 ..and so on..
 }}}
-
-Is the algorithm semi-decidable?
-
-Derivation when normalisation of locals uses flexible tyvars, too - simulates the effect of (!SkolemOccurs):
-{{{
-[F v] ~ v  ||-  [F v] ~ v
-==> normalise
-v ~ [x2], F v ~ x2  ||-  v ~ [x1], F v ~ x1
-** x2 := F v
-==> (Local) with v
-F [x2] ~ x2  ||-  [x2] ~ [x1], F [x2] ~ x1
-** x2 := F v
-==> normalise
-F [x2] ~ x2  ||-  x2 ~ x1, F [x2] ~ x1
-** x2 := F v
-==> 2x (Top) & Unify
-[F x1] ~ x1  ||-  [F x1] ~ x1
-** x1 := F v
-==> normalise
-x1 ~ [y2], F x1 ~ y2  ||-  x1 ~ [y1], F x1 ~ y1
-** x1 := F v, y2 := F x1
-..we stop here if (Local) doesn't apply to flexible tyvars
-}}}
-
-Problem is that with rank-n signatures, we do want to use (Local) with flexible tyvars.
+My guess is that the algorithm terminates for all satisfiable queries.  If that is correct, the entailment problem that the algorithm solves would be  semi-decidable.
+