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

[Martin Sulzmann]

I was talking about *static* termination. Hence, the conditions
in the paper and the new one I proposed are of course incomplete.
I think that's your worry, isn't it? There are reasonable 
type-level programs which are rejected but will terminate for certain
goals. 

I think what you'd like is that each instance specifies its own
termination condition which can then be checked dynamically.
Possible but I haven't thought much about it. The simplest and most
efficient strategy seems to stop after n number of steps.

Martin


Roman Leshchinskiy writes:
 > 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