Add a variant of discontinue with effects

[michaelleejl]

It seems strange to me that we can match an expression with:

1. A value
2. An exception
3. An effect

But we can resume a continuation only by continue-ing with a value or discontinue-ing with an exception.

This seems to me a strange asymmetry, though perhaps it has been previously discussed and rejected for some reason that I'm missing.

I've implemented the feature as discontinue_with_effect. This is, in my opinion, not the optimal name, since the meaning of with is different to the meaning of with in discontinue_with_backtrace. I'm happy to hear alternative proposals. Some other I considered include:

1. reperform
2. discontinue_using_effect

[nojb]

@fpottier @kc do you have an opinion on this proposal?

[kayceesrk]

I remember proposing this while building multicore OCaml, and @lpw25 had good reasons against it. That this is not compositional. I can't seem to recall the specific reasons now.

[fpottier]

I have indeed noted this asymmetry; the handler can cause perform to produce a normal outcome or an exceptional outcome but not an "effect" outcome. I don't know whether this asymmetry was intentional in the designers' minds.

This limitation does possibly make it easier to reason (formally) about programs. In the paper by Paulo de Vilhena and myself on Separation Logic for effect handlers, and in Osiris (work in progress whose aim is to build a Separation Logic for OCaml), each effect is described by a precondition and a postcondition, where the postcondition describes just the values that can be returned and the exceptions that can be raised; there is no need to describe which other effects can be performed. I have not given serious thought to the changes that would be required if it was possible to resume a continuation with an effect. Such a feature would require changes both in the semantics and in the program logic.

Are there any real-world examples where this feature seems desirable? I think I would very much like to see motivating examples before moving to extend the language with such a feature.

[kayceesrk]

There’s some prior work on bidirectional effects, which may be relevant to this discussion: https://dl.acm.org/doi/10.1145/3428207. I would also very much like to see examples.

[gasche]

I naively wonder if this is what the mysterious "reperform" runtime instruction does.

[kayceesrk]

reperform is the catch-all case in a handler. If none of the patterns match in an effect handler, we (re)perform the effect to forward it to the outer handler and return the value or the exception to the original performer. It is described briefly in the last paragraph of section 4.1 in https://dl.acm.org/doi/10.1145/3453483.3454039.

[michaelleejl]

One possible example, perhaps a little contrived (since discontinue does suffice), would be when using effects to find the right place to perform an effect. As an example, consider let insertion (the example is adapted from Oleg's gengenlet.ml, by @yallop).

Here's how one would use MetaOCaml to perform a form of naïve let insertion, where one uses a handler to manually mark a point where the expression should be inserted, and an effect simply performs the insertion

let let_locus body = 
  try body with 
  effect LetInsert (v), k -> .< let x = .~v in .~(continue k .< x >.)>.

Here's a cleverer version, which tries to insert as high as possible -- by finding the first handler where the expression is not fully bound (so the lowest insertion point that is too high), and then insert one level lower

let let_locus body =
  try body () with
    effect (LetInsert v) k when not (is_well_scoped v) ->
    (* Inserting it here would generate ill-scoped code. *)
    discontinue k Unhandled
  | effect (LetInsert v) k ->
    match perform (LetInsert v) with
    | v ->
      (* Successful insertion higher up. *)
      continue k v
    | exception Unhandled ->
      (* Insert it here *)
      .< let x = .~v in .~(continue k .< x >.)>.

I think, with discontinue_with_effect, you might be able to reuse the first, naïve implementation in the second, cleverer implementation, as follows:

let let_locus body =
 try body () with
   effect (FindInsertionPoint v), k when not (is_well_scoped v) ->
   discontinue_with_effect k (LetInsert v)
 | effect (FindInsertionPoint v), k ->
   match perform (FindInsertionPoint v) with
   | v ->
     continue k v
   | effect LetInsert (v), k' ->
     (* Insert it here *)
     .< let x = .~v in .~(continue k' .< x >.)>.

Notice that the handler for perform (FindInsertionPoint e) is the naïve implementation. I think this makes sense -- you use the FindInsertionPoint effect to find the right place to perform the effect, and then use discontinue to perform the effect at the right place. Using an exception rather than an effect feels (to me) like an anti-pattern: nothing exceptional has actually occurred.

[fpottier]

It seems to me that the last two examples that you give have very similar structure; I don't see a significant gain by moving from the use of an exception to the use of an effect.

I can understand your argument that "using an exception is an anti-pattern", but I view it as more philosophical than technical. In fact, pushing the philosophical argument further, I would say that perhaps both exceptions and effects are mis-used in this let-insertion example. An approach that would be more efficient and (in my opinion) simpler (as it does not use any control effects) is to store a set of let bindings that are waiting to be inserted in a (mutable) priority queue. The priority of a binding let x = e would be the maximum free variable of the expression e, where variables are represented as de Bruijn indices. Thus, every time a let_locus combinator is exited, the bindings that must be inserted at this point can be easily and efficiently extracted out of the priority queue.

[fpottier]

To implement my suggestion, it may be necessary to extend MetaOCaml with an operation that compares two code fragments by determining which one has the most-recently-bound free variable. Thinking twice, I am not sure that this makes sense, because this depends on the order in which the variables will be bound in the future. In summary, my suggestion is only half-baked, but I do think that it is worth thinking about this let-insertion problem as an algorithmic problem and to avoid the temptation of abusing the control constructs of the host language (OCaml).

[michaelleejl]

I'm in complete agreement with you that there is no structural difference, and that any difference between effects and exceptions in this case are philosophical rather than technical.

I hadn't considered thinking about let-insertion as an algorithmic problem. My initial feeling is that reasoning is complicated because one only knows, retrospectively, when one has passed a point where some bindings must have been inserted (one must wait for the future to become the past). To my mind, this implies needing an ability to re-enter scope, which perhaps explains why it's tempting to abuse effects, even if there are other ways to implement it.

I think @yallop might be better placed to comment on this, but I agree that structurally and technically, there isn't much of a difference between exceptions and effects (which is why I commented that the example might be a bit contrived).

(I raised the PR mostly because I find the asymmetry interesting, rather than having a concrete problem in mind.)