|
|
```wiki
|
|
|
|
|
|
|
|
|
=== Problem with Plan MS: Termination is still an issue ===
|
|
|
|
|
|
Example:
|
|
|
|
|
|
F and G are type function constructors. Consider the local assumptions
|
|
|
|
|
|
F (G Int) = Int -- (1)
|
|
|
G Int = F (G Int) -- (2)
|
|
|
|
|
|
Applying (2) on (1) yields
|
|
|
|
|
|
F (G Int) = Int
|
|
|
--> F (F (G Int)) = Int
|
|
|
--> F (F (F (G Int))) = Int
|
|
|
--> ...
|
|
|
|
|
|
NOTE:
|
|
|
Plan MC rejects (2), cause the type equation is non-decreasing.
|
|
|
Here we are after a more liberal type checking method.
|
|
|
|
|
|
=== Plan MS revised overview ===
|
|
|
|
|
|
Plan MS only works if we "normalize" terms. Effectively, we represent
|
|
|
terms via CHR constraints, "term reductions" are then performed via
|
|
|
CHR solving steps.
|
|
|
|
|
|
The big picture:
|
|
|
|
|
|
Step 1 (normal form step):
|
|
|
|
|
|
(a) We transform local and wanted type equations to CHR constraints.
|
|
|
(b) We transform type instances to CHR simplification rules.
|
|
|
|
|
|
Step 2 (solving step):
|
|
|
|
|
|
To derive wanted from local type equations wrt type instances,
|
|
|
we perform CHR solving steps. These CHR solving steps can be mapped
|
|
|
to "term reduction" steps.
|
|
|
|
|
|
|
|
|
The advantage of this method is that we can deal with
|
|
|
"non-terminating" local type equations (see above) and
|
|
|
"non-confluent" local type equations, e.g.
|
|
|
S Int = Int /\ S Int = F Int, and we don't need to orient
|
|
|
type equations.
|
|
|
Of course, we need to impose the usual conditions on
|
|
|
type instances, ie termination and confluence.
|
|
|
|
|
|
=== CHR vs Term reductions ===
|
|
|
|
|
|
How to phrase term reduction steps in terms of CHR solving steps.
|
|
|
The main task is to put terms into normal from.
|
|
|
|
|
|
==== Normal form =====
|
|
|
|
|
|
Terms are formed as follows
|
|
|
|
|
|
t ::= a -- variable
|
|
|
| F -- type function constructor
|
|
|
| T -- ordinary type constructor
|
|
|
| t t -- type application
|
|
|
|
|
|
Type equations are formed as follows
|
|
|
|
|
|
Eq ::= t = t
|
|
|
| Eq /\ Eq
|
|
|
|
|
|
|
|
|
Type equations can easily be put into the following normal form
|
|
|
|
|
|
n ::= a
|
|
|
| T
|
|
|
| n n
|
|
|
|
|
|
C ::= a = n
|
|
|
| F n = n
|
|
|
| C /\ C
|
|
|
|
|
|
|
|
|
a set of type equations in normal form C, consists of equations of
|
|
|
the form a = n or F n = n where the normal form type n does not refer
|
|
|
to type function constructors.
|
|
|
|
|
|
|
|
|
Example:
|
|
|
|
|
|
The normal form of
|
|
|
|
|
|
F (G Int) = Int
|
|
|
G Int = F (G Int)
|
|
|
|
|
|
from above is
|
|
|
|
|
|
F a = Int
|
|
|
G Int = a
|
|
|
G Int = b
|
|
|
F b = c
|
|
|
G Int = c
|
|
|
|
|
|
The first two equations are derived from F (G Int) = Int. That is, we
|
|
|
replace G Int by a where a is a fresh wobbly variable.
|
|
|
The last three equations result from replacing G Int on the rhs of
|
|
|
G Int = F (G Int) by b which leads to G Int = F b, then we replace
|
|
|
F b by c and we are done.
|
|
|
|
|
|
NOTE: We consider a, b, c as wobbly type variables.
|
|
|
|
|
|
|
|
|
Similarly, we build the normal form of type instances.
|
|
|
For example, the normal form of
|
|
|
|
|
|
forall a. F [a] = [F a]
|
|
|
|
|
|
is
|
|
|
|
|
|
forall a. exists b. F [a] = b /\ b=[F a]
|
|
|
|
|
|
|
|
|
NOTE:
|
|
|
|
|
|
We must build the normal form of type instances. Otherwise, application of
|
|
|
type instances may break the normal form property. Eg. consider
|
|
|
application of forall a. F [a] = [F a]
|
|
|
on F [Int] = b /\ S Int = b.
|
|
|
|
|
|
It should be clear that a normal form equation such as F a = Int,
|
|
|
can be viewed as the CHR constraint F a Int, and
|
|
|
forall a. exists b. F [a] = [b] /\ b=F a as
|
|
|
the CHR simplification
|
|
|
rule F [a] [b] <==> F a b
|
|
|
|
|
|
|
|
|
==== Mapping CHR derivations to term derivations and vice versa ====
|
|
|
|
|
|
|
|
|
Let t1=t1' /\ .... /\ tk=tk' be a set of type equations and
|
|
|
C its normal form. Let TT be a set of type instances and
|
|
|
TT_n its normal form.
|
|
|
|
|
|
We build a canonical form of t1=t1' /\ .... /\ tk=tk'
|
|
|
by solving C wrt rules TT_n plus the standard FD rule, ie
|
|
|
C -->* C'. This CHR derivation can be mapped to a term derivation
|
|
|
t1=t1' /\ .... /\ tk=tk' -->* t1''=t1''' /\ ... /\ tl''=tl'''
|
|
|
(ie a sequence of rule applications using the FC type equation rules).
|
|
|
|
|
|
|
|
|
The CHR solving steps in detail:
|
|
|
|
|
|
FD solving step:
|
|
|
|
|
|
Let C \equiv C' /\ F n1 = n2 /\ F n1 = n3.
|
|
|
|
|
|
Then, C --> C' /\ F n1 = n2 /\ n2 = n3
|
|
|
|
|
|
In the above, we still use the (normal form) term representation.
|
|
|
In the CHR constraint notation, the FD solving step is written
|
|
|
|
|
|
C' /\ F n1 n2 /\ F n1 n3
|
|
|
--> C /\ F n1 n2 /\ n2 = n3
|
|
|
|
|
|
The point is that the "actual" type equations only contain
|
|
|
normal form types.
|
|
|
|
|
|
This solving step can be mapped back to a term reduction step.
|
|
|
Let t1''=t1''' /\ ... /\ tl''=tl''' be the term representation
|
|
|
of C' /\ F n1 = n2 /\ n2 = n3 (ie we remove the wobbly variables
|
|
|
we've introduced earlier in the normal form step).
|
|
|
Then,
|
|
|
|
|
|
t1=t1' /\ .... /\ tk=tk' --> t1''=t1''' /\ ... /\ tl''=tl'''
|
|
|
|
|
|
this is now a term reduction step
|
|
|
(using the type equation rules of the FC system)
|
|
|
|
|
|
|
|
|
Type instance step:
|
|
|
|
|
|
Let C \equiv C' /\ F n1 = n2
|
|
|
|
|
|
and forall a. F n3 = n4 /\ C in TT_n such that
|
|
|
phi(n3) = n1 for some substitution phi where dom(phi)=a.
|
|
|
|
|
|
Then, C --> C' /\ phi(n4) = n2 /\ phi(C).
|
|
|
|
|
|
As before, we also give the derivation in CHR constraint notation.
|
|
|
C' /\ F n1 n2
|
|
|
--> C' /\ phi(n4) = n2 /\ phi(C)
|
|
|
|
|
|
This solving step can be mapped back to a term reduction step
|
|
|
(a type instance application step).
|
|
|
|
|
|
|
|
|
Equivalence step:
|
|
|
|
|
|
The FD and type instance step introduce equations among normal form types.
|
|
|
We build the mgu of these normal form equations (for this step it's
|
|
|
helpful to use the CHR constraint notation).
|
|
|
|
|
|
|
|
|
=== Plan MS revised details ===
|
|
|
|
|
|
Let TT be a set of type instances,
|
|
|
C and W a set of constraints already in normal form where
|
|
|
C are the local equations and W are the wanted equations.
|
|
|
|
|
|
We check that W follows from C wrt TT as follows.
|
|
|
|
|
|
We rewrite (C | W) to (C' | W') by performing the following steps.
|
|
|
|
|
|
Reduce C step:
|
|
|
Apply FD and CHR simp steps on C, ie C -->* C', we obtain
|
|
|
|
|
|
(C | W) --> (C' | W)
|
|
|
|
|
|
Reduce W type instance step
|
|
|
Apply CHR simp steps on W, ie W -->* W', we obtai
|
|
|
|
|
|
|
|
|
(C | W) --> (C | W')
|
|
|
|
|
|
NOTE: we could also apply FD steps on W, no harm.
|
|
|
|
|
|
Reduce W wrt C step:
|
|
|
|
|
|
If C \equiv C' /\ F n1 = n2 and W \equiv F n1 = n3 /\ W'
|
|
|
then
|
|
|
|
|
|
(C | W) --> (C | W' /\ n2 = n3)
|
|
|
|
|
|
|
|
|
We exhaustively apply the above steps (if TT is terminating the steps
|
|
|
are terminating). That is,
|
|
|
|
|
|
(C | W) -->* (C' | W')
|
|
|
|
|
|
then check if W' is a subset of C'. If yes, W follows from C wrt TT.
|
|
|
|
|
|
NOTE:
|
|
|
|
|
|
In the reduce W wrt C step, adding n2 = n3 to C as well is wrong.
|
|
|
We could also first reduce C -->* C', then
|
|
|
C' /\ W -->* C'' and check that C'' and C' are equivalent (by exploiting
|
|
|
the fact that C implies W iff C <-> C /\ W).
|
|
|
|
|
|
|
|
|
==== A note on efficiency ====
|
|
|
|
|
|
The normal from representation has the advantage that searching for
|
|
|
"matchings" becomes "easier". Eg in case of the (earlier) plan MS and plan MC,
|
|
|
given the local assumption S s1 ... sn = t we traverse/search all
|
|
|
terms to find matching partners S s1 ... sn which then will be replaced by t.
|
|
|
Consider the local G Int = Int and the term [Tree [G Int]] where we first
|
|
|
traverse two list nodes and a tree node before we find the matching partner.
|
|
|
In the normal from representation, we use a "flat" representation, all potential
|
|
|
matchings must be at the "outer" level. We could even use hashing. That is,
|
|
|
the local F a = Int is assigned the hash index F, so is the wanted
|
|
|
constraint F a = Int (trivial example). When applying locals/type functions
|
|
|
we'll only need to consider the entries with hash index F.
|
|
|
|
|
|
|
|
|
==== A note on evidence construction ====
|
|
|
|
|
|
We yet need to formalize the exact details how to map CHR evidence back
|
|
|
to term evidence. In fact, there's an issue.
|
|
|
Consider the type equation (with evidence)
|
|
|
|
|
|
e : F (G Int) = Int
|
|
|
|
|
|
In the normal form representation, the above is represented as
|
|
|
|
|
|
e1 : F a = Int
|
|
|
e2 : G Int = a
|
|
|
|
|
|
for some evidence e1 and e2. What's the connection between e and e1,e2?
|
|
|
|
|
|
In case e : F (G Int) = Int is wanted, the method outlined above
|
|
|
will attempt to find evidence for e1 and e2. Given e1 and e2 we can then
|
|
|
build evidence e.
|
|
|
|
|
|
In case e : F (G Int) = Int is local (ie given), the normal form construction
|
|
|
seems to be the wrong way around. Indeed, from e we can't necessarily build e1 and e2.
|
|
|
Well, the method outlined here simply assumes that
|
|
|
e1 : F a = Int, e2 : G Int = a
|
|
|
is the internal representation for
|
|
|
e : F (G Int) = Int
|
|
|
|
|
|
NOTE:
|
|
|
|
|
|
The user can of course use the more "compact" term representation of local assumptions,
|
|
|
but internally we'll need to keep local assumptions in normal form.
|
|
|
|
|
|
|
|
|
``` |
|
|
\ No newline at end of file |