On Mon, 2006-02-27 at 16:43 +0800, Martin Sulzmann wrote:
I was talking about *static* termination. Hence, the conditions in the paper and the new one I proposed are of course incomplete.
Just to clarify: by static you mean verifiable at instance definition time (i.e. under the open world assumption) whereas dynamic is when the instance is used (i.e. in a closed world)? Note that both are "static" from a programmer's point of view, but this terminology definitely makes sense here.
I think that's your worry, isn't it? There are reasonable type-level programs which are rejected but will terminate for certain goals.
My worry are type-level programs which are rejected but will provably terminate for *all* goals.
I think what you'd like is that each instance specifies its own termination condition which can then be checked dynamically.
That depends on what you mean by specifying a termination condition. Suppose we want to solve C t1 ... tn = t. A possible rule might be: if while solving this we ever come up with the goal C u1 ... un = u, then the number of constructors in u1 ... un must be strictly less than the number of constructors in t1 ... tn. Something similar to this should guarantee termination but would still allow structural recursion on types. Note that this doesn't even have to be fully dynamic - it can be checked once per module by using instance declarations as generators, I think.
Possible but I haven't thought much about it. The simplest and most efficient strategy seems to stop after n number of steps.
Yes, but I don't really like that. Any n will be completely arbitrary and rule out perfectly good type-level programs for no good reason. For what it's worth, this is essentially what C++ does and people don't like it and seem to largely ignore the limit specified in the standard. Roman