... | ... | @@ -66,7 +66,7 @@ where |
|
|
|
|
|
- the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families,
|
|
|
- the left-hand side of an equality may not occur in the right-hand side, and
|
|
|
- the relation `x > y` is a total order on type variables, where `alpha > a` whenever `alpha` is a flexible and `a` a rigid type variable (otherwise, the total order may be aribitrary).
|
|
|
- the relation `x > y` is an arbitrary, but total order on type variables.
|
|
|
|
|
|
|
|
|
The second bullet of the where clause is trivially true for equalities of Form (1); it also implies that the left- and right-hand sides are different.
|
... | ... | @@ -144,8 +144,7 @@ flatten [[F t1..tn]] = (alpha, [[id :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn) |
|
|
(t1', eqt1) = flatten t1
|
|
|
..
|
|
|
(tn', eqtn) = flatten tn
|
|
|
FRESH alpha, such that alpha > x for all x already used
|
|
|
RECORD alpha := F t1'..tn'
|
|
|
FRESH alpha
|
|
|
flatten [[t1 t2]] = (t1' t2', eqs++eqt)
|
|
|
where
|
|
|
(t1', eqs) = flatten t1
|
... | ... | @@ -154,17 +153,12 @@ flatten t = (t, []) |
|
|
```
|
|
|
|
|
|
|
|
|
The substitutions `RECORD`ed during `flatten` need to be (unconditionally) applied during finalisation (i.e., the 3rd phase).
|
|
|
|
|
|
|
|
|
Notes:
|
|
|
|
|
|
- Perform Rule Triv as part of normalisation.
|
|
|
- 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.)
|
|
|
- We flatten locals and wanteds in the same manner, using fresh flexible type variables. (We have flexibles in locals anyway and don't use (Unify) during normalisation - this is different to `new-single`.)
|
|
|
|
|
|
**TODO** We may want to drop the `alpha > x for all x already used` side condition on fresh `alpha`s again. Instead, we should probably consider all *local* flexible variable equalities during finalisation, too. At least, those involving flexible variables introduced by flattening.
|
|
|
|
|
|
## Propagation (aka Solving)
|
|
|
|
|
|
|
... | ... | @@ -195,177 +189,259 @@ co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s |
|
|
co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
|
|
|
```
|
|
|
|
|
|
where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable. **SLPJ: why this restriction? I thought we were treating
|
|
|
where `co1` may be a wanted only if `co2` is a wanted, too.
|
|
|
</td></tr></table>
|
|
|
|
|
|
>
|
|
|
> NB: Afterwards, we need to normalise `co2'`. Then, the SubstVarVar or SubstVarFam rules may apply to the results of normalisation. Moreover, `co1` may have a SubstFam or a SubstVarFam match with rules other than the results of normalising `co2'`.
|
|
|
|
|
|
<table><tr><th>**SubstVarVar**</th>
|
|
|
<td>```wiki
|
|
|
co1 :: x ~ t & co2 :: x ~ s
|
|
|
=(SubstVarVar)=>
|
|
|
co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
|
|
|
```
|
|
|
|
|
|
where `co1` may be a wanted only if `co2` is a wanted, too.
|
|
|
</td></tr></table>
|
|
|
|
|
|
>
|
|
|
> NB: Afterwards, we need to normalise `co2'`. Then, the SubstVarVar or SubstVarFam rules may apply to the results of normalisation, but not with `co1`, as `s` and `t` cannot contain `x` -- cf. the definition of normal equalities. However, `co1` may have another SubstVarVar or SubstVarFam match with rules other than the results of normalising `co2'`.
|
|
|
|
|
|
flexible and rigid variables the same.****
|
|
|
NB: Afterwards, we need to normalise `co2'`. Then, the SubstVarVar or SubstVarFam rules may apply to the results of normalisation. Moreover, `co1` may have a SubstFam or a SubstVarFam match with rules other than the results of normalising `co2'`.
|
|
|
**SubstVarVar**co1 :: x \~ t & co2 :: x \~ s
|
|
|
=(SubstVarVar)=\>
|
|
|
co1 :: x \~ t & co2' :: t \~ s with co2 = co1 \|\> co2'
|
|
|
where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable.
|
|
|
<table><tr><th>**SubstVarFam**</th>
|
|
|
<td>```wiki
|
|
|
co1 :: x ~ t & co2 :: F s1..sn ~ s
|
|
|
=(SubstVarFam)=>
|
|
|
co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s with co2 = [co1/x](F s1..sn) |> co2'
|
|
|
```
|
|
|
|
|
|
NB: Afterwards, we need to normalise `co2'`. Then, the SubstVarVar or SubstVarFam rules may apply to the results of normalisation, but not with `co1`, as `s` and `t` cannot contain `x` -- cf. the definition of normal equalities. However, `co1` may have another SubstVarVar or SubstVarFam match with rules other than the results of normalising `co2'`.
|
|
|
**SubstVarFam**co1 :: x \~ t & co2 :: F s1..sn \~ s
|
|
|
=(SubstVarFam)=\>
|
|
|
co1 :: x \~ t & co2' :: \[t/x\](F s1..sn) \~ s with co2 = \[co1/x\](F s1..sn) \|\> co2'
|
|
|
where `x` occurs in `F s1..sn`. (`co1` may be local or wanted.)
|
|
|
</td></tr></table>
|
|
|
|
|
|
>
|
|
|
> NB: No normalisation required. Afterwards, SubstVarVar or SubstVarFam may apply to `co1` and all rules, except SubstVarVar, may apply to `co2'`. However, SubstVarFam cannot again apply to `co1` and `co2'`, as `t` cannot contain `x` -- cf. the definition of normal equalities.
|
|
|
|
|
|
|
|
|
NB: In the three substitution rules, it is never necessary to try using `co1` with any of the equalities derived from `co2'`. Hence, after having considered one equality as `co1` with every other equality, we can immediately put `co1` into the list of residual equalities.
|
|
|
|
|
|
### Rule application: specification
|
|
|
|
|
|
|
|
|
NB: No normalisation required. Afterwards, SubstVarVar or SubstVarFam may apply to `co1` and all rules, except SubstVarVar, may apply to `co2'`. However, SubstVarFam cannot again apply to `co1` and `co2'`, as `t` cannot contain `x` -- cf. the definition of normal equalities..
|
|
|
**SLPJ**: why distinguish SubstVarVar and SubstVarFam. The paper has only one rule**.
|
|
|
**Rule application: specification
|
|
|
Propagation proceeds by applying any of the four rules until the system does not change anymore. After application of a rule, the equalities that were modified need to be normalised again:
|
|
|
Propagate = fix (Top \| SubstFam \| SubstVarVar \| SubstVarFam)
|
|
|
Rule application: algorithm
|
|
|
|
|
|
```wiki
|
|
|
Propagate = fix (Top | SubstFam | SubstVarVar | SubstVarFam)
|
|
|
```
|
|
|
|
|
|
### Rule application: algorithm
|
|
|
|
|
|
|
|
|
The following function gets a list with all local and wanted equalities. It returns a list of residual equalities that permit no further rule application.
|
|
|
|
|
|
```wiki
|
|
|
-- all four rule functions return Nothing if rule not applicable
|
|
|
applyTop :: RewriteInst -\> Maybe EqInst
|
|
|
applySubstFam :: RewriteInst -\> RewriteInst -\> Maybe EqInst -- return only...
|
|
|
applySubstVarVar :: RewriteInst -\> RewriteInst -\> Maybe EqInst -- ...the modified...
|
|
|
applySubstVarFam :: RewriteInst -\> RewriteInst -\> Maybe EqInst -- ...equality
|
|
|
applyTop :: RewriteInst -> Maybe EqInst
|
|
|
applySubstFam :: RewriteInst -> RewriteInst -> Maybe EqInst -- return only...
|
|
|
applySubstVarVar :: RewriteInst -> RewriteInst -> Maybe EqInst -- ...the modified...
|
|
|
applySubstVarFam :: RewriteInst -> RewriteInst -> Maybe EqInst -- ...equality
|
|
|
|
|
|
propagate :: \[RewriteInst\] -\> \[RewriteInst\]
|
|
|
propagate eqs = snd (prop eqs \[\])
|
|
|
propagate :: [RewriteInst] -> [RewriteInst]
|
|
|
propagate eqs = snd (prop eqs [])
|
|
|
where
|
|
|
prop :: \[RewriteInst\] -\> \[RewriteInst\] -\> \[RewriteInst\]
|
|
|
prop \[\] res = res
|
|
|
prop :: [RewriteInst] -> [RewriteInst] -> [RewriteInst]
|
|
|
prop [] res = res
|
|
|
prop (eq:eqs) res = apply eq eqs res
|
|
|
|
|
|
apply eq@\[\[co :: F t1..tn \~ t\]\] eqs res
|
|
|
\| Just eq' \<- applyTop eq = prop (norm eq' ++ eqs) res
|
|
|
\| otherwise = mapRule (applySubstFam eq) -- TODO!!!
|
|
|
ObservationsOnly SubstVarFam when replacing a variable in a family equality can lead to recursion with (Top).
|
|
|
A significant difference to `new-single` is that solving is a purely local operation. We never instantiate any flexible variables.
|
|
|
We cannot discard any variable equalities after substitution since we do not substitute into right-hand sides anymore. Moreover, in the concrete implementation, variables may also be re-introduced due to simplification of type classes (which currently doesn't happen in the same iteration).
|
|
|
Finalisation
|
|
|
apply eq@[[co :: F t1..tn ~ t]] eqs res
|
|
|
| Just eq' <- applyTop eq = prop (norm eq' ++ eqs) res
|
|
|
| otherwise = mapRule (applySubstFam eq) -- TODO!!!
|
|
|
```
|
|
|
|
|
|
### Observations
|
|
|
|
|
|
- Only SubstVarFam when replacing a variable in a family equality can lead to recursion with (Top).
|
|
|
- A significant difference to `new-single` is that solving is a purely local operation. We never instantiate any flexible variables.
|
|
|
- We cannot discard any variable equalities after substitution since we do not substitute into right-hand sides anymore. Moreover, in the concrete implementation, variables may also be re-introduced due to simplification of type classes (which currently doesn't happen in the same iteration).
|
|
|
|
|
|
## Finalisation
|
|
|
|
|
|
|
|
|
If only flexible type equalities remain as wanted equalities, the locals entail the wanteds. We can now instantiate type variables in flexible type equalities where possible to propagate constraints into the environment. In GHC, we may wrap any remaining equalities (of any form) into an implication constraint to be propagated outwards (where it may be solved under an extended set of local equalities.)
|
|
|
|
|
|
|
|
|
Notes:
|
|
|
(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.)
|
|
|
|
|
|
- (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.)
|
|
|
|
|
|
---
|
|
|
|
|
|
**TODO** Still need to adapt example to new rule set!
|
|
|
|
|
|
**TODO** Now that we delay instantiation until after solving, do we still need to prioritise flexible variables equalities over rigid ones? (Probably not.) In any case, we need to handle variable-variable equalities (at least of flexibles) specially during finalisation. Even if they locals, they need to be taken into account during finalisation. (Otherwise, we may miss some instantiations of flexibles that occur in the environment.)
|
|
|
ExamplesSubstituting wanted family equalities with SubstFam is crucial if the right-hand side contains a flexible type variableTop: F Int \~ \[Int\]
|
|
|
|
|
|
\|- F delta \~ \[delta\], F delta \~ \[Int\]
|
|
|
## Examples
|
|
|
|
|
|
### Substituting wanted family equalities with SubstFam is crucial if the right-hand side contains a flexible type variable
|
|
|
|
|
|
```wiki
|
|
|
Top: F Int ~ [Int]
|
|
|
|
|
|
|- F delta ~ [delta], F delta ~ [Int]
|
|
|
(SubstFam)
|
|
|
\|- F delta \~ \[delta\], norm \[\[ \[delta\] \~ \[Int\] \]\]
|
|
|
==\>
|
|
|
\|- F delta \~ \[delta\], delta \~ Int
|
|
|
|- F delta ~ [delta], norm [[ [delta] ~ [Int] ]]
|
|
|
==>
|
|
|
|- F delta ~ [delta], delta ~ Int
|
|
|
(SubstVar)
|
|
|
\|- norm \[\[ F Int \~ \[Int\] \]\], delta \~ Int
|
|
|
==\>
|
|
|
\|- F Int \~ \[Int\], delta \~ Int
|
|
|
|- norm [[ F Int ~ [Int] ]], delta ~ Int
|
|
|
==>
|
|
|
|- F Int ~ [Int], delta ~ Int
|
|
|
(Top)
|
|
|
\|- norm \[\[ \[Int\] \~ \[Int\] \]\], delta \~ Int
|
|
|
==\>
|
|
|
\|- delta \~ Int
|
|
|
|- norm [[ [Int] ~ [Int] ]], delta ~ Int
|
|
|
==>
|
|
|
|- delta ~ Int
|
|
|
QED
|
|
|
Interaction between local and wanted family equalities
|
|
|
```
|
|
|
|
|
|
### Interaction between local and wanted family equalities
|
|
|
|
|
|
|
|
|
Example 4 of Page 9 of the ICFP'09 paper.
|
|
|
F \[Int\] \~ F (G Int) \|- G Int \~ \[Int\], H (F \[Int\]) \~ Bool
|
|
|
=(norm)=\>
|
|
|
F \[Int\] \~ a, F b \~ a, G Int \~ b
|
|
|
\|-
|
|
|
G Int \~ \[Int\], H x \~ Bool, F \[Int\] \~ x
|
|
|
(SubstFam w/ F \[Int\])
|
|
|
F \[Int\] \~ a, F b \~ a, G Int \~ b
|
|
|
\|-
|
|
|
G Int \~ \[Int\], H x \~ Bool, x \~ a
|
|
|
|
|
|
```wiki
|
|
|
F [Int] ~ F (G Int) |- G Int ~ [Int], H (F [Int]) ~ Bool
|
|
|
=(norm)=>
|
|
|
F [Int] ~ a, F b ~ a, G Int ~ b
|
|
|
|-
|
|
|
G Int ~ [Int], H x ~ Bool, F [Int] ~ x
|
|
|
(SubstFam w/ F [Int])
|
|
|
F [Int] ~ a, F b ~ a, G Int ~ b
|
|
|
|-
|
|
|
G Int ~ [Int], H x ~ Bool, x ~ a
|
|
|
(SubstFam w/ G Int)
|
|
|
F \[Int\] \~ a, F b \~ a, G Int \~ b
|
|
|
\|-
|
|
|
b \~ \[Int\], H x \~ Bool, x \~ a
|
|
|
F [Int] ~ a, F b ~ a, G Int ~ b
|
|
|
|-
|
|
|
b ~ [Int], H x ~ Bool, x ~ a
|
|
|
(SubstVar w/ x)
|
|
|
F \[Int\] \~ a, F b \~ a, G Int \~ b
|
|
|
\|-
|
|
|
b \~ \[Int\], H a \~ Bool, x \~ a
|
|
|
F [Int] ~ a, F b ~ a, G Int ~ b
|
|
|
|-
|
|
|
b ~ [Int], H a ~ Bool, x ~ a
|
|
|
```
|
|
|
|
|
|
**TODO** If we use flexible variables for the flattening of the wanteds, too, the equality corresponding to `x ~ a` above will be oriented the other way around. That can be a problem because of the asymmetry of the SubstVar and SubstFun rules (i.e., wanted equalities are not substituted into locals).
|
|
|
TerminationSkolemOccurs
|
|
|
|
|
|
## Termination
|
|
|
|
|
|
### 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 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\]
|
|
|
\[F v\] \~ v \|\|- \[F v\] \~ v
|
|
|
|
|
|
```wiki
|
|
|
E_t: forall x. F [x] ~ [F x]
|
|
|
[F v] ~ v ||- [F v] ~ v
|
|
|
```
|
|
|
|
|
|
**New-single**: The following derivation shows how the algorithm in new-single fails to terminate for this example.
|
|
|
\[F v\] \~ v \|\|- \[F v\] \~ v
|
|
|
==\> normalise
|
|
|
v \~ \[a\], F v \~ a \|\|- v \~ \[x\], F v \~ x
|
|
|
|
|
|
```wiki
|
|
|
[F v] ~ v ||- [F v] ~ v
|
|
|
==> normalise
|
|
|
v ~ [a], F v ~ a ||- v ~ [x], F v ~ x
|
|
|
a := F v
|
|
|
==\> (Local) with v
|
|
|
F \[a\] \~ a \|\|- \[a\] \~ \[x\], F \[a\] \~ x
|
|
|
==\> normalise
|
|
|
F \[a\] \~ a \|\|- x \~ a, F\[a\] \~ x
|
|
|
==\> 2x (Top) & Unify
|
|
|
\[F a\] \~ a \|\|- \[F a\] \~ a
|
|
|
==> (Local) with v
|
|
|
F [a] ~ a ||- [a] ~ [x], F [a] ~ x
|
|
|
==> normalise
|
|
|
F [a] ~ a ||- x ~ a, F[a] ~ x
|
|
|
==> 2x (Top) & Unify
|
|
|
[F a] ~ a ||- [F a] ~ a
|
|
|
..and so on..
|
|
|
```
|
|
|
|
|
|
**New-single using flexible tyvars to flatten locals, but w/o Rule (Local) for flexible type variables**: With (SkolemOccurs) it is crucial to avoid using Rule (Local) with flexible type variables. We can achieve a similar effect with new-single 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
|
|
|
|
|
|
```wiki
|
|
|
[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 failing tests in the testsuite 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
|
|
|
==\> normalise
|
|
|
v \~ \[a\], F v \~ a \|\|- v \~ \[x\], F v \~ x
|
|
|
|
|
|
```wiki
|
|
|
[F v] ~ v ||- [F v] ~ v
|
|
|
==> normalise
|
|
|
v ~ [a], F v ~ a ||- v ~ [x], F v ~ x
|
|
|
a := F v
|
|
|
==\> (IdenticalLHS) with v & F v
|
|
|
v \~ \[a\], F v \~ a \|\|- \[a\] \~ \[x\], x \~ a
|
|
|
==\> normalise
|
|
|
v \~ \[a\], F v \~ a \|\|- x \~ a, x \~ a
|
|
|
==\> (Unify)
|
|
|
v \~ \[a\], F v \~ a \|\|- a \~ a
|
|
|
==\> normalise
|
|
|
v \~ \[a\], F v \~ a \|\|-
|
|
|
==> (IdenticalLHS) with v & F v
|
|
|
v ~ [a], F v ~ a ||- [a] ~ [x], x ~ a
|
|
|
==> normalise
|
|
|
v ~ [a], F v ~ a ||- x ~ a, x ~ a
|
|
|
==> (Unify)
|
|
|
v ~ [a], F v ~ a ||- a ~ a
|
|
|
==> normalise
|
|
|
v ~ [a], F v ~ a ||-
|
|
|
QED
|
|
|
```
|
|
|
|
|
|
|
|
|
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
|
|
|
==\> normalise
|
|
|
v \~ \[a\], F v \~ a \|\|- v \~ \[x\], F v \~ x
|
|
|
|
|
|
```wiki
|
|
|
[F v] ~ v ||- [F v] ~ v
|
|
|
==> normalise
|
|
|
v ~ [a], F v ~ a ||- v ~ [x], F v ~ x
|
|
|
a := F v
|
|
|
==\> (Local) with F v
|
|
|
v \~ \[a\], F v \~ a \|\|- v \~ \[x\], x \~ a
|
|
|
==\> (Unify)
|
|
|
v \~ \[a\], F v \~ a \|\|- v \~ \[a\]
|
|
|
==\> (Local) with v
|
|
|
v \~ \[a\], F \[a\] \~ a \|\|- \[a\] \~ \[a\]
|
|
|
==\> normalise
|
|
|
v \~ \[a\], F \[a\] \~ a \|\|-
|
|
|
==> (Local) with F v
|
|
|
v ~ [a], F v ~ a ||- v ~ [x], x ~ a
|
|
|
==> (Unify)
|
|
|
v ~ [a], F v ~ a ||- v ~ [a]
|
|
|
==> (Local) with v
|
|
|
v ~ [a], F [a] ~ a ||- [a] ~ [a]
|
|
|
==> normalise
|
|
|
v ~ [a], F [a] ~ a ||-
|
|
|
QED
|
|
|
```
|
|
|
|
|
|
**One problems remains**: The algorithm still fails to terminate for unsatisfiable queries.
|
|
|
\[F v\] \~ v \|\|- \[G v\] \~ v
|
|
|
==\> normalise
|
|
|
v \~ \[a\], F v \~ a \|\|- v \~ \[x\], G v \~ x
|
|
|
|
|
|
```wiki
|
|
|
[F v] ~ v ||- [G v] ~ v
|
|
|
==> normalise
|
|
|
v ~ [a], F v ~ a ||- v ~ [x], G v ~ x
|
|
|
a := F v
|
|
|
==\> (Local) with v
|
|
|
F \[a\] \~ a \|\|- \[a\] \~ \[x\], G \[a\] \~ x
|
|
|
==\> normalise
|
|
|
F \[a\] \~ a \|\|- x \~ a, G \[a\] \~ x
|
|
|
==\> (Unify)
|
|
|
F \[a\] \~ a \|\|- G \[a\] \~ a
|
|
|
==\> (Top)
|
|
|
\[F a\] \~ a \|\|- G \[a\] \~ a
|
|
|
==\> normalise
|
|
|
a \~ \[b\], F a \~ b \|\|- G \[a\] \~ a
|
|
|
==> (Local) with v
|
|
|
F [a] ~ a ||- [a] ~ [x], G [a] ~ x
|
|
|
==> normalise
|
|
|
F [a] ~ a ||- x ~ a, G [a] ~ x
|
|
|
==> (Unify)
|
|
|
F [a] ~ a ||- G [a] ~ a
|
|
|
==> (Top)
|
|
|
[F a] ~ a ||- G [a] ~ a
|
|
|
==> normalise
|
|
|
a ~ [b], F a ~ b ||- G [a] ~ a
|
|
|
b := F a
|
|
|
..and so on..
|
|
|
```
|
|
|
|
|
|
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.
|
|
|
Download in other formats:[Plain Text](/trac/ghc/wiki/TypeFunctionsSolving?version=71&format=txt)[](http://trac.edgewall.org/)Powered by [Trac 1.2.2](/trac/ghc/about)
|
|
|
|
|
|
By [Edgewall Software](http://www.edgewall.org/).Visit the Trac open source project at
|
|
|
[http://trac.edgewall.org/](http://trac.edgewall.org/)**</td></tr></table> |
|
|
\ No newline at end of file |
|
|
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. |