Changes between Version 27 and Version 28 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 3, 2008 9:55:16 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v27 v28  
    134134=== !SkolemOccurs ===
    135135
    136 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.
    137 
    138 To see how the new algorithm handles the type of equalities that required !SkolemOccurs in the ICFP'08 algorithm, consider the following notorious example:
     136The 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.
     137
     138To look at this in more detail, let's consider the following notorious example:
    139139{{{
    140140E_t: forall x. F [x] ~ [F x]
     
    142142}}}
    143143
    144 Derivation with rules in the new-single report:
     144'''New-single''': The following derivation shows how the algorithm in new-single fails to terminate for this example.
    145145{{{
    146146[F v] ~ v  ||-  [F v] ~ v
     
    157157}}}
    158158
    159 Same, but de-prioritise (Local) - i.e., (Local) applies only if nothing else does:
     159'''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.
     160{{{
     161[F v] ~ v  ||-  [F v] ~ v
     162==> normalise
     163v ~ [x2], F v ~ x2  ||-  v ~ [x1], F v ~ x1
     164** x2 := F v
     165==> (Local) with v
     166F [x2] ~ x2  ||-  [x2] ~ [x1], F [x2] ~ x1
     167** x2 := F v
     168==> normalise
     169F [x2] ~ x2  ||-  x2 ~ x1, F [x2] ~ x1
     170** x2 := F v
     171==> 2x (Top) & Unify
     172[F x1] ~ x1  ||-  [F x1] ~ x1
     173** x1 := F v
     174==> normalise
     175x1 ~ [y2], F x1 ~ y2  ||-  x1 ~ [y1], F x1 ~ y1
     176** x1 := F v, y2 := F x1
     177..we stop here if (Local) doesn't apply to flexible tyvars
     178}}}
     179A 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).
     180
     181'''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.)
    160182{{{
    161183[F v] ~ v  ||-  [F v] ~ v
     
    174196}}}
    175197
    176 Same, but de-prioritise (Local) rewriting with equalities of Forms (2) & (3):
     198In fact, it is sufficient to de-prioritise Rule (Local) for variable equalities (if it is used for other equalities at all):
    177199{{{
    178200[F v] ~ v  ||-  [F v] ~ v
     
    191213}}}
    192214
    193 Problem is that we still fail to terminate for unsatisfiable queries:
     215'''One problems remains''': The algorithm still fails to terminate for unsatisfiable queries.
    194216{{{
    195217[F v] ~ v  ||-  [G v] ~ v
     
    210232..and so on..
    211233}}}
    212 
    213 Is the algorithm semi-decidable?
    214 
    215 Derivation when normalisation of locals uses flexible tyvars, too - simulates the effect of (!SkolemOccurs):
    216 {{{
    217 [F v] ~ v  ||-  [F v] ~ v
    218 ==> normalise
    219 v ~ [x2], F v ~ x2  ||-  v ~ [x1], F v ~ x1
    220 ** x2 := F v
    221 ==> (Local) with v
    222 F [x2] ~ x2  ||-  [x2] ~ [x1], F [x2] ~ x1
    223 ** x2 := F v
    224 ==> normalise
    225 F [x2] ~ x2  ||-  x2 ~ x1, F [x2] ~ x1
    226 ** x2 := F v
    227 ==> 2x (Top) & Unify
    228 [F x1] ~ x1  ||-  [F x1] ~ x1
    229 ** x1 := F v
    230 ==> normalise
    231 x1 ~ [y2], F x1 ~ y2  ||-  x1 ~ [y1], F x1 ~ y1
    232 ** x1 := F v, y2 := F x1
    233 ..we stop here if (Local) doesn't apply to flexible tyvars
    234 }}}
    235 
    236 Problem is that with rank-n signatures, we do want to use (Local) with flexible tyvars.
     234My 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.
     235