[Haskell-cafe] (Un)termination of overloading resolution

[Martin Sulzmann]

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

Your example violates this condition

 > 	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 = (((->) (() -> ()))) ()

this leads to

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 ()) :: ())