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

[Roman Leshchinskiy]

On Mon, 27 Feb 2006, Martin Sulzmann wrote:
> > > 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
> >
> > I'm probably misunderstanding something but doesn't this imply that we
> > cannot declare any instances for
> >
> >   class C a b | a -> b, b -> a
> >
> > which do not break the bound variable condition? This would remove one
> > of the main advantages fundeps have over associated types.
> >
>
> Sure you can. For example,
>
> class C a b | a->b, b->a
> instance C [a] [a]

Ah, sorry, my question was very poorly worded. What I meant to say was 
that there are no instances declarations for C which satisfy your rule 
above and, hence, all instances of C (or of any other class with 
bidirectional dependencies) must satisfy the other, more restrictive 
conditions. Is that correct?

> In your example below, you are not only breaking the Bound Variable
> Condition, but you are also breaking the Coverage Condition.

Yes, but I'm breaking the rule you suggested only once :-) It was only 
intended as a cute example. My worry, however, is that there are many 
useful type-level programs similar to my example which are guaranteed to 
terminate but which nevertheless do not satisfy the rules in your paper or 
the one you suggested here. I think ruling those out is unavoidable if you 
want to specify termination rules which every instance must satisfy 
individually. But why not specify rules for sets of instances instead? 
This is, for instance, what some theorem provers do for recursive 
functions and it allows them to handle a wide range of those without 
giving up decidability.

Roman