Function instrumentation and effect handlers transformation

[CAG2Mark]

Instrumentation of functions

Allows functions executions to be suspended by creating an associated continuation class with each function / lambda body which can be resumed. The continuation class are intended to be chained together with other functions' continuation classes to create a "heapified" structured stack frame.

The main idea is to treat functions as a state machine, with state transitions occurring at all possibly effectful function calls. More state transitions may be inserted to support various kinds of control flow, such as if/while.

At each possibly effectful function call, functions will check if the result of that call is a continuation. If so, it will capture its current stack frame into a continuation, including the current state in the state machine, and append it onto the other continuation.

Effect handlers

Use the above instrumentation of functions to compile effect handlers such as:

handle h = Effect with
  fun perform(arg)(k) = k(arg); arg
in foo(h)

Most of the additional infrastructure needed to compile handlers are in the Predef. Nested handlers, and handlers within other handlers, are also supported. This part was mostly done by @AnsonYeung

TODO

• Verify our implementation's semantics against other implementations

[AnsonYeung]

the rationale of this is that x may not be initialized if the handler is non-resumptive

[LPTK]

Ah, good point... For now it's fine like this, then. But later when we have optional bindings, we can mark it as optional.

[AnsonYeung]

For class constructors, the old example code was due to the reliance of implicitly returning this in the constructor. I've modified it to explicitly return the correct this in the continuation class.

TODO:

• Check Instantiate for effects

[LPTK]

Again, I think this should be a runtime crash. Or we should forbid handlers in ctors. It's obviously wrong to return an object instance that's only partly initialized.

That said, maybe we could catch this in the type system (checking that the handler is resumptive).

[AnsonYeung]

So the current implementation interprets this as same as

class Lol() with
  "b"

because handlers are handled in the function. Changes to elaboration is required to fix this if the intended behaviour is to break out of the constructor as consider the following currently equivalent code:

class Lol() with
  handle h = Effect with
    fun perform(arg)(k) =
      print(arg)
      "b"
  in
    print(h.perform("k"))
    val x = 123
  val y = 1234 // the constructor continues here

My point is that x is never supposed to be a field here even if the handler is resumptive. Having a field that may or may not exist depending on control flow seems weird (it could be something like a optional field that always exist instead).

btw, the problem is actually not related to handlers inherently. For example:

module M with
  if true then
    val a = 1
    ()
  else
    val b = 2
    ()

Now M.a always exist but M.b does not (in the generated JS code). Note that true can be replaced by anything. The exact problem occur in classes as well.

We should give the same treatment to if and handlers whatever semantics is desired. If we need to reject handlers in constructors we need to reject ifs in constructor for the same reason too and I don't think there is actually any difference here.

[LPTK]

My point is that x is never supposed to be a field here even if the handler is resumptive.

I disagree. Because it is a val binding syntactically in the body of the class, it is a field of the class.

Having a field that may or may not exist depending on control flow seems weird

This should never be the case.

btw, the problem is actually not related to handlers inherently. For example:

module M with
  if true then
    val a = 1
    ()
  else
    val b = 2
    ()

Now M.a always exist but M.b does not (in the generated JS code). Note that true can be replaced by anything. The exact problem occur in classes as well.

Here a and b clearly aren't fields of M. They're just local bindings inside local blocks of the constructor. Avoiding this kind of confusion is actually one reason I've been considering disallowing val in local blocks.

Notice the error here:

object Foo with
  if true then
    val x = 1
    ()

Foo.x
//│ ╔══[ERROR] Object 'Foo' does not contain member 'x'
//│ ║  l.37: 	Foo.x
//│ ╙──      	   ^^
//│ = 1

The fact that it still compiles to a field and returns 1 at the end is an elaborator bug.

we need to reject ifs in constructor for the same reason

Absolutely not!

To be clear, what I'm proposing is to reject handle statements (ie without an in body) in ctors.

[LPTK]

Do you guys @CAG2Mark and @AnsonYeung intend to address the remaining issues quickly so we can finally merge this? I don't think you want to wait until after I merge the symbol changes (it would give you more work to fix things).

[LPTK]

All right, I think we can merge now. There are still unresolved things to address in future PRs, though. I'll open a tracking issue for them.