[Haskell-cafe] (Un)termination of overloading resolution
rl at cse.unsw.EDU.AU
Mon Feb 27 00:42:39 EST 2006
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.
More information about the Haskell-Cafe