[Haskell-cafe] (Un)termination of overloading resolution
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
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 ()) :: ())
More information about the Haskell-Cafe
mailing list