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