Handlers don't mix with recursion

[Lysxia]

As a simplified example, consider exceptions. We can throw exceptions with lift Fail, and we have a handler to catch them: catch : itree (failureE +' E) R -> itree E R -> itree E R. On exception, carry on with the second itree E R.

Intuitively, the pseudocode program below should succeed, because the Fail exception will be caught.

let f true = catch (f false) (ret tt)
    f false = Fail
in f true

Now we can try to implement it in Coq, with rec to handle recursion. It would look more or less like this:

let f := rec (fun b : bool =>
  if b then catch (lift (Call false) (* <- f false *)) (ret tt)
       else lift Fail)
in
f true

Unexpectedly, this will throw an exception. The reason is that the recursive call, Call, is an effect like any other, and the handler catch ignores anything that's not Fail. Hence, the then branch is equivalent to lift (Call false).

I'm still trying to understand what is happening, and looking for workarounds. This just came up while I was formalizing CCS using itrees (on the ccs branch), where parallel composition and message hiding are currently implemented as handlers, but allowing recursive terms results in a nesting of those handlers with rec like above.

That behavior is quite unintuitive. At first sight this seems plain wrong, that's just not how exceptions work. However this behavior also seems oddly similar to the approach of a POPL19 paper: Abstraction-Safe Effect Handlers via Tunneling https://www.cs.cornell.edu/andru/papers/tunnel-eff/tunnel-eff.pdf

The idea is to statically associate effects with a handler: an effectful function a -> E b is really a function parameterized by a handler for E. (Whereas the traditional interpretation of effects is dynamic: an effect is handled by the closest suitable handler in the call stack.)

In the example above, lift Fail can be understood as being bound to some handler outside the rec definition, which is why the catch handler in the other branch doesn't see it. Thus, one idea to make rec more flexible may be to attach handlers to the Call constructor, but I don't see an easy way to avoid doing so manually.

The reason things don't appear to be as bad in the POPL paper is that they also have a rule that, when calling an effectful function (such as f false in the then branch of f true), its effects are handled by the lexically closest handler (which would be catch in this case). But we can't easily import that idea in itrees because recursive functions are treated quite differently.

[gmalecha]

I think I ran into this a few months ago as well. I agree that it is counter-intuitive. It is a general issue about effect handlers, but the real issue, as you point out, is the fact that it leaks the implementation details of fix since people don't think of fixpoints as effects (and indeed, if you use cofix directly rather than fix then you don't have this problem).

[Lysxia]

I guess this is going to be a long term issue to discuss on a paper about "Programming with algebraic effects in Coq using ITrees". The Coq-io project is relevant to look at.