=== 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.