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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
