Martin Sulzmann sulzmann at comp.nus.edu.sg
Tue Feb 21 23:33:20 EST 2006

```This is not a counter-example to my conjecture.
Let's consider the general case (which I didn't
describe in my earlier email).

In case we have an n-ary type function T
(or (n+1)-ary type class constraint T)
the conditions says
for each

type T t1 ... tn = t

(or rule T t1 ... tn x ==> t)

then rank(ti) > rank(t) for each i=1,..,n

> 	class E m a b | m a -> b
> 	instance E m (() -> ()) (m ())

The improvement rule says:

rule E m (() -> ()) x ==> x=(m ())

but rank m < rank (m ())

Your example shows that the condition

rank(t1)+...+rank(tn) > rank(t)

is not sufficient (but that's not a surprise).

Program text
> test = foo (\f -> (f ()) :: ()) (\f -> (f ()) :: ())
gives rise to

Foo ((->) (() -> ())) ((() -> ()) -> ())

via
> instance (E m a b, Foo m b) => Foo m (a->()) where

this constraint reduces to

E ((->) (() -> ())) (()->()) x
Foo ((->) (() -> ())) x

the above improvement yields x = (((->) (() -> ()))) ()

Foo ((->) (() -> ())) ((((->) (() -> ()))) ())

and so on (the second component is increasing).

So, I'll stick to my claim. I don't think I have time
at the moment to work out the details of my claim/proof sketch.
But if somebody is interested. The following is a good
reference how to attack the problem:
@inproceedings{thom-term,
author = "T. Fr{\"u}hwirth",
title = "Proving Termination of Constraint Solver Programs",
booktitle = "Proc.\ of New Trends in Constraints: Joint {ERCIM/Compulog} Net
Workshop",
volume = "1865",
series = "LNAI",
publisher = "Springer-Verlag",
year = "2000"
}

Martin

oleg at pobox.com writes:
>
> Martin Sulzmann wrote:
>
> > - The type functions are obviously terminating, e.g.
> >   type T [a] = [[a]] clearly terminates.
> > - It's the devious interaction between instances/superclasss
> >   and type function which causes the type class program
> >   not to terminate.
> >
> > Is there a possible fix? Here's a guess.
> > For each type definition in the AT case
> >
> > type T t1 = t2
> >
> > (or improvement rule in the FD case
> >
> > rule T1 t1 a ==> a=t2
> >
> > we demand that the number of constructors in t2
> > is strictly smaller than the in t1
> > (plus some of the other usual definitions).
>
> I'm afraid that may still be insufficient, as the following
> counter-example shows. It causes GHC 6.4.1 to loop in the typechecking
> phase. I haven't checked the latest GHC. The example corresponds to a
> type function (realized as a class E with functional dependencies) in
> the context of an instance. The function in question is
>
> 	class E m a b | m a -> b
> 	instance E m (() -> ()) (m ())
>
> We see that the result of the function, "m ()" is smaller (in the
> number of constructors) that the functions' arguments, "m" and
> "() -> ()" together. Plus any type variable free in the result is also
> free in at least one of the arguments. And yet it loops.
>
>
>
> {-# OPTIONS -fglasgow-exts #-}
> -- Note the absence of the flag -fallow-undecidable-instances
>
> module F where
>
> class Foo m a where
>     foo :: m b -> a -> Bool
>
> instance Foo m () where
>     foo _ _ = True
>
> instance (E m a b, Foo m b) => Foo m (a->()) where
>     foo m f = undefined
>
> class E m a b | m a -> b where
>     tr :: m c -> a -> b
>
> -- There is only one instance of the class with functional dependencies
> instance E m (() -> ()) (m ()) where
>     tr x = undefined
>
> -- GHC(i) loops
>
> test = foo (\f -> (f ()) :: ()) (\f -> (f ()) :: ())
```