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

[Roman Leshchinskiy]

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