# Changes between Version 27 and Version 28 of TypeFunctionsSolving

Show
Ignore:
Timestamp:
08/03/08 02:55:16 (5 years ago)
Comment:

--

Unmodified
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