Prompt not found caused by bidirectional/higher-order `resume` leaking local handler

[kyay10]

It seems that I've broken effect safety... The examples below fail with Prompt not found x

It seems that the type of resume, when there are bidirectional effects or explicit computation arguments (which are ultimately equivalent), is incorrect, and incorrect in such a way as to break effect safety.

The (boxed) type of resume is illuminating as to what the issue is:

// for the first 2 examples
resume: {{() => Unit} => Unit} => (() => Unit at {io}) at {}
// for the third example
resume: {() => Unit / { Yield }} => Unit at {io,this}

Specifically, the parameter it takes in is a computation of arbitrary effects/captures. That's exactly the issue! Any local effects added inside an effect implementation can leak through resume, and the handler is none the wiser because it is unaware of those local handlers. Instead, resume's parameter should be a first-class function, that can only capture the things that resume captures. In other words, it should be like:

// for the first 2 examples
resume: ({() => Unit} => Unit at {}) => (() => Unit at {io}) at {}
// for the third example
resume: (() => Unit / { Yield } at {io, this}) => Unit at {io,this}

Resumptions obtained at a prompt only have their outer handlers in their capture set, which is fine. Then, though, you have this ability to insert a brand new middle handler, which is fine too, but then when you resume inside that middle handler, the middle handler leaks into the resumption, without being mentioned in its type. Crucially, this middle handler can be very easily removed by boxing a resumption and resuming it outside that middle handler. Middle handlers alone aren't the issue; the issue is that your resumption can, all of a sudden, depend on them. I hope that makes some sense. The code showcases the issue clearly, but this explanation should hopefully motivate my remedy for this.

Examples: Using a passed-in computation (i.e. a "higher order effect"):

interface Greet { def sayHello(): Unit }

interface Foo {
  def yield(): Unit
  def foo{prog: () => Unit}: Unit
}

def helloWorld() at {io} = { 
  val f: () => Unit at {io} = try {
    do foo { do yield() }
    val f2: () => Unit at {io} = box { }
    f2
  } with Foo {
    def yield() = box { resume(())() }
    def foo() = try { resume {{prog} => prog(); do sayHello() } } with Greet { 
      def sayHello() = box { println("hi") }  // not tail resumptive to prevent optimization
    }
  }
  f()
}

Using bidirectional effects:

interface Greet { def sayHello(): Unit }
interface Yield {
  def yield(): Unit
}
interface Foo {
  def foo(): Unit / Yield
}

def helloWorld() at {io} = { 
  val f: () => Unit at {io} = try {
    do foo()
    val f2: () => Unit at {io} = box { }
    f2
  } with Foo {
    def foo() = try { resume { do yield(); do sayHello() } } with Greet { 
      def sayHello() = box { println("hi") }  // not tail resumptive to prevent optimization
    }
  } with Yield {
    def yield() = box { resume(())() }
  }
  f()
}

Bidirectional effects with a region (which makes the code a bit more sane)

interface Greet { def sayHello(): Unit }
interface Yield {
  def yield(): Unit
}
interface Foo {
  def foo(): Unit / Yield
}

def helloWorld() at {io} = region this { 
  var later: Unit => Unit at {io, this} in this = box { _ => }
  try {
    do foo()
  } with Foo {
    def foo() = try { resume { do yield(); do sayHello() } } with Greet { 
      def sayHello() = println("hi") // not tail resumptive to prevent optimization
    }
  } with Yield {
    def yield() = later = box resume
  }
  later(())
}

The common thread between them all is that, before do sayHello() is reached, the code captures the continuation through yield, and resumes the continuation completely outside of the try block that Foo originated in. This is okay for Foo since its prompt is captured in there, but it's not okay for Greet since it's a local handler.

Original reproducer

```effekt import option import dequeue

interface Abort { def exit(): Nothing }

interface Scheduler { def yield(): Unit def launch { p: () => Unit }: Unit }

def scheduler { prog: {Scheduler} => Unit } = region this { var queue: Dequeue[() => Unit at {this, prog}] in this = emptyQueue(); def run(): Unit = queue.popBack match { case None() => () case Some((k, q)) => queue = q k(); run() } try { prog {s} } with s: Scheduler { def yield() = { queue = queue.pushFront(box { resume(()) }) } def launch() = { queue = queue .pushFront(box { resume { {prog} => () } }) .pushFront(box { try { resume { {prog} => prog(); do exit() } } with Abort { def exit() = () } }) } } run() }

interface Send[T] { def send(value: T): Unit }

interface Receive[T] { def receive(): T }

type Either[A, B] { Left(a: A) Right(b: B) }

def channel[T]{receiver: => Unit / Receive[T]} {sender: => Unit / Send[T]}: Unit = region this { scheduler { {s} => var queue: Either[Dequeue[T => Unit at {this, receiver, sender, s}], Dequeue[(Unit => Unit at {this, receiver, sender, s}, T)]] in this = Right(emptyQueue()); s.launch { try { sender() } with Send[T] { def send(value) = { queue match { case Left(l) => l.popBack match { case None() => queue = Right(emptyQueue().pushFront((box resume, value))) case Some((receive, l2)) => queue = Left(l2) s.launch { receive(value) } s.launch { resume(()) } } case Right(r) => queue = Right(r.pushFront((box resume, value))) } } } } try { receiver() } with Receive[T] { def receive() = { queue match { case Right(r) => r.popBack match { case Some(((ack, value), r2)) => queue = Right(r2) s.launch { resume(value) } s.launch { ack(()) } case None() => queue = Left(emptyQueue().pushFront(box resume)) } case Left(l) => queue = Left(l.pushFront(box resume)) } } } } }

def main() = { channel[Int]{ println(1) println(do receiveInt) println(4) println(do receiveInt) } { println(2) do send(3) println(5) do send(6) println(7) } }

</details>

[jiribenes]

Hi, thanks for the report!

This is likely a miscompilation [?], but interestingly, it also happens when I compile it with effekt --no-optimize (and on LLVM) 🤔 cc @b-studios

The following lines look a bit suspicious to me:

        .pushFront(box {
          try { resume { {prog} => prog(); do exit() } } with Abort {
            def exit() = ()
          }
        })

What would you expect to be the output of this program? Just 1\n2\n3\n4? 🤔

EDIT: We're working on the issue 🚧🔨 👀

[kyay10]

I'm pretty sure now it's not a miscompilation. I'm preparing a small reproducer, but basically the type of resume (when there's bidirectional effects, or the effect takes in a computation type) is incorrect, and thus results in accidentally leaking a local handler.

My original code was effect-unsafe, I just didn't realize in the moment, but the issue is, the compiler didn't realize either.

[kyay10]

I've updated with a simpler example to show the issue. It seems to require both boxing (to dynamically remove a prompt) and bidirectional effects (for resume to have the incorrect type) EDIT: I've made further updates to show why resume's type is the culprit here, and how to remedy it.

[kyay10]

FYI, here's an example (check the "Details" section) of code that, if changed around, may exhibit the same bug:

  def twice[R](default: R) = {
    var other: Option[R] = None()
    resume { { p: => R / Nd } =>
      hnd { p() } match {
        case Cons(el1, Cons(el2, _)) => 
          other = Some(el2);
          el1
        case Nil() => default        
      }
    }
    resume { {p: => R / Nd} =>
      other match {
        case Some(v) => v
        case None() => default
      }
    }
  }

Can you spot it? other is leaked into the resumption, and p is arbitrary, so it can easily "undo" other. This is really, really bad. I haven't tested this, but I conjecture that, if you massage it right, either 1) It'll fail immediately at runtime, or 2) It won't fail because it'll just hold onto a reference to the relevant stack, but it'll exhibit very strange behaviour w.r.t. backtracking. Either way, this is definitely undefined behaviour. The fix in this example would be to allocate other in some higher region.

EDIT: it seems we're firmly in (2) territory, at least running in the JS playground. I'm trying to get the strange backtracking behaviour (as in, local state that is "forgotten about", thus effectively global state)

EDIT: It took me a while, but I finally did it! It really is (2): state backtracking can break completely? The main difficulty was that local state inside a handler would usually just allocate in the same arena as the handler, so the state was backtracked properly. I needed to move the state inside of a (non-trivial, but useless) handler so that it doesn't get backtracked properly. Here's the code The really sinister thing is that this doesn't even error! Effect safety is broken, but we don't even get a helpful Prompt not found, instead, we get completely incorrect results. I know the code for this is rather convoluted, but I hope that you can see that maybe, somewhere out there, someone might run something like this and get legitimately incorrect behaviour.

[b-studios]

Hey @kyay10, thanks for all of these very insightful examples and reproductions!

Indeed it looks like there is a bug in our implementation when it comes to typing bidirectional resumptions. This part is a bit fragile in the implementation. Bidirectional effects, block parameters on effects and block parameters on methods are all very similar; also in that their implementation is still fragile and an underused part of the language 😅

I do not believe it is a fundamental (that is theoretical) problem, though, "just" an implementation issue. We will definitely look into it ASAP and your examples will be instrumental for this. Thanks again!

[kyay10]

@b-studios I (very respectfully) disagree, tentative on what a "theoretical problem" is, and with full acknowledgement that I may be very wrong, especially since I didn't design this language 😅

Let me make this concrete. The following is a pathological example that demonstrates this issue (playground):

effect escape(): Nothing
effect yield(): Unit
effect bi(): Unit / yield

def test() at {}: Unit = try {
  do bi()
  box {}
} 
with yield { box { resume(())() } }
with bi {
  try {
    resume { 
      do yield()
      do escape()
    }
  } with escape { box {} }
}()

(We can vary this easily to use a region instead of returning functions, as shown earlier in this conversation. We can also vary this to use block parameters instead of bidirectional effects).

Here's what I vaguely imagine this translates to (pseudo-effekt, but also somewhat kotlin-y syntax, with captures still denoted as usual):

def test() at {}: Unit {
  val f = reset[() => Unit at {}] { {prompt} =>
    val y: yield at prompt = new yield { prompt.shift { k: (Unit => (() => Unit at {}) at {}) => box { 
      val f3 = k(())
      // 6
      f3() 
} } }
    val b: bi at prompt = new bi { {y2} =>
      val f2: {yield} => Unit = prompt.shift { k: ({{yield} => Unit} => (() => Unit at {})) =>
        reset[() => Unit at {}] { {prompt2} =>
          val e: escape at prompt2 = new escape { prompt2.shift { box {} } }
          k { {y3} => 
            // 4
            y3.yield()
            // 5
            e.escape()
          }
        }
      }
      // 3
      f2{y}
    }
    b.bi{y}
    // 2
    box {}
  }
  // 1
  f()
}

(All the y<n>s are the same, so I won't differentiate them moving forward) If reading Effekt papers has taught me anything, it's that effects should be reasoned about through the stack.

Stack visualization proving this program is unsound, regardless of any bugs in the compiler/runtime

upon entering b.bi{y}:

caller of test()	test at // 1	prompt	f at // 2

upon entering b's call to shift:

caller of test()	test at // 1	prompt	f at // 2	b at // 3

The shift happens, so now we have k:

prompt	f at // 2	b at // 3

and our stack is:

caller of test()	test at // 1

Then we perform the reset for prompt2 (assuming some TCO to make the stack shorter):

caller of test()	test at // 1	prompt2

Then we resume k (The newest (rightmost) frame represents the block we resumed with. Everything else is just k appended to the current stack):

caller of test()	test at // 1	prompt2	prompt	f at // 2	b at // 3	f2 at // 4

Now's the cool part. We call y3.yield, and inside of its shift, we get:

k:

prompt	f at // 2	b at // 3	f2 at // 5

stack:

caller of test()	test at // 1	prompt2

Crucially, k gets wrapped up in a boxed function, which is returned. Thus we pop the stack to continue with that boxed function. Popping the stack simply pops any prompt frames, and gives the value thus to the first non-prompt frame, which we find here:

caller of test()	test at // 1

importantly, prompt2 is gone.

Thus we run the boxed function, and right when we reach the call to its k (which is the latest k shown above), the stack looks like:

caller of test()	y at // 6

so we resume k with (). The stack now looks like (before () is actually propagated through):

caller of test()	y at // 6	prompt	f at // 2	b at // 3	f2 at // 5

So now we run // 5, which tries to shift to prompt2, which doesn't exist on the stack...

So this program must be rejected, but where exactly is the problem? I see 2 places (both implying a mistyped resume, and mistyped in a rather fundamental way in that some normal parameters should be block parameters):

1. b's shift (which is what I was arguing for in earlier comments
2. y's shift (which maybe is what you are advocating for)

Specifically, for (1), k (shift's lambda parameter) should have type ({yield} => Unit at {}) => (() => Unit at {}), as in it takes a boxed function with the same captures as reset captures (in this case, none). This change rejects this example since escape (and any such "middle" handler (i.e., a handler added in a shift) cannot be leaked out of its shift. This does, however, rule out a class of (advanced) programs that want to install handlers in shift and have them available for their bidirectional resumption.

for (2), k should be a block parameter, and hence should be of type Unit => (() => Unit at {}) (no captures because it's a block param). As a result, y's body would get rejected since the boxed function it attempts to return captures k, but the expected type has no captures. The idea here is that, if an interface has bidirectional effects, its resumptions (i.e. the parameters to shift's lambda) should always be passed in as block parameters, and hence they can't leak and accidentally undo a middle handler. Note that I'm not suggesting we just disable boxing completely for them, since it should still be valid to pass those resumptions around, as long as they're used within the handler's body. This rules out a class of programs that doesn't use middle handlers, but wishes to box some resumptions to use them outside a handler's body.

(1) seems more apt to me because middle handlers seem rare to me. (2) feels too limiting to apply indiscriminately to any interface with bidirectional effects (because also, I should clarify, the restrictions on shift's k, that is being a block parameter and thus less useful, would apply to "sister handlers" as well, as in handlers that use the same prompt).

There's a more complicated option (3): give the user choice between (1) and (2) for each try they write. Maybe you choose one of them as the default, and have a soft keyword to switch it to the other, or something like that.

As an educated guess, I believe most effect-safe frameworks that have "local resumptions", as in this ability to inject code at the call site of an effect, simply just disallow using middle handlers. I have played around with using monadic regions for effect-safe shift/reset (which, IIRC, scala-effekt did something similar?) and my local resumptions weren't explicitly a feature, but instead just "happen" by returning a thunk and thawing it immediately. Such a program is not typeable in my framework because, in the "thawing it immediately" step, the current region is only known to support prompt, but not prompt2. Since I have no type-changing magic (answer-type polymorphism, is that what it's called? but with changing the type of a region, I guess), the call-site of shift doesn't change its region information based on what happens inside the shift, and so the effects that a local resumption can do are limited to any bidirectional effects, the prompt itself (which, funnily enough, effekt doesn't support, see #1180), and anything that the prompt captures. This is the same solution as (1) here. You set in stone the effects allowed for your local resumptions, but you allow any explicitly-passed-in bidirectional effects. What you don't allow is middle handlers, because escaping them is easy.

[phischu]

I am deeply impressed by your knowledge of this topic in general as well as of specific Effekt internals. Thank you for this thorough report. Your analysis is correct, but let me rephrase it so we are on the same page. Let's consider your example again:

effect escape(): Nothing
effect yield(): Unit
effect bi(): Unit / yield

def test() at {}: Unit =
  try {
    do bi()
    box {}
  } with yield { () =>
    def resume1 at {} = resume
    box { resume(())() }
  } with bi { () =>
      def resume2 at {} = resume
      try {
        resume { 
          do yield()
          do escape()
        }
      } with escape { box {} }
  }()

I have given names to the two resumptions, so we can activate capture inlay hints and look at them. resume1 has captures {} and resume2 has captures {}. But this is wrong! When thinking about this operationally, (and your stack drawings are great for this), then bi will install a fresh handler very time it is called (non-scoped resumption), and use the capability escape under resume { ... }. So when the sister handler for yield capture the resumption, it excludes the freshly-installed prompts, but it does contain the future call to escape.

In non-bidirectional handlers, the capture of the resumption is the capture of the handled statements, unioned with the catpure of all handler implementations. Currently, in bidirectional handlers it is the same. The fix I propose is to also union this with the capture of the statements we are resuming with, i.e. { do yield(); do escape() }. This should rule out this program, because escape is not even in scope in the handler for yield. Do you believe this would solve the general problem?

[kyay10]

@phischu Thank you, first of all! I've been into effect handlers the past couple of years, with the goal of implementing then in Kotlin, and Effekt, in particular, has had a large impact on my understanding. So, I owe my understanding to your team and their great papers!

I believe this would solve the problem, but I'm kinda struggling to see how the types would make any sense. The capture for escape would be referring to a handler that's not even lexically in scope (as in, in every other case, I believe a capture refers to something that you'd have access to in an effect-unsafe language, as in the names in the capture set are names lexically in scope).

Let's assume that's fine for now. Here's a potential issue: if we represent that capture as "the escape coming from line blah", I think there could be a risk of someone basically fusing yield and bi together so that they're one effect, and then the resumption is called where "the escape coming from line blah" is available, but it's actually a different escape coming from a different invocation of bi (with a different prompt and everything). I've modified the code to show this fused effect:

effect escape(): Nothing
effect bi(yield: Bool){yieldRef: () => Unit}: Unit

def test() at {}: Unit = try {
  do bi(false) { do bi(true) {} }
  box {}
} 
with bi { yield =>
  try {
    if (yield) box { resume{ {_} => () } () }
    else resume { {yieldRef} => 
      yieldRef()
      do escape()
    }
  } with escape { box {} }
}()

My point is that the escape will differ between bi calls. However, I can't find a way to exploit this (the fused example wouldn't compile under your proposal because the unboxing right after try is not valid since "the escape coming from line blah" is not in scope); that doesn't mean it's guaranteed to be safe, though, but at least it'd require a rather pathological program to trigger this issue. I think the struggle with replicating it is because there's a Voldemort type (well, a Voldemort capture) that makes it hard to pass resumptions between these different calls to bi. I can't return something with that capture easily, and I can't make an outer local variable whose type has that capture (I can make one inside bi's implementation, but I then can't share that variable between bi calls).

This would effectively be like (1) from above, but without its disadvantage, so it really is the best of both worlds. In fact, it's "auto-switching" between (1) and (2) in some sense. I really like that!

One final thing to keep in mind is that your proposal might accidentally rule out this completely valid program:

effect escape(): Nothing
effect yield(): Unit
effect bi(): Unit / yield

def test() at {}: Unit = try {
  do bi()
  ()
} 
with yield { (box resume)(()) }
with bi {
  try {
    resume { 
      do yield()
      do escape()
    }
  } with escape { () }
}

if yield's body isn't allowed to unbox things with an escape capture, then resume in yield can never be boxed then unboxed, even if that'd be valid. Just something to keep in mind.

(Does Effekt even have a way to capture an effect? I thought captures were only to block parameters)

[b-studios]

I (very respectfully) disagree, tentative on what a "theoretical problem" is, and with full acknowledgement that I may be very wrong, especially since I didn't design this language

Don't worry :) Respectful disagreements is how we make progress.

Again, thanks for the excellent analysis. Especially the last example and the stack trace make things very obvious. I also have to second @phischu that it is very impressive that you manage to navigate this whole space elegantly.

First of all, let me try to address this question

(Does Effekt even have a way to capture an effect? I thought captures were only to block parameters)

As you probably know, Effekt translates to capability passing, such as follows:

effect escape(): Nothing
effect yield(): Unit
effect bi{y: yield}: Unit

def main() at {}: Unit = {
  val f =
    try {
      b.bi{y}
      box {}
    }
    with b: bi {
      try {
        resume { {y} =>
          y.yield()
          e.escape()
        }
      } with e: escape { box {} }
    }
    with y: yield { box { resume(())() } }
  f()
}

It is now clear that capabilities like b, y, and e can occur in captures. In the source language, we make up fresh names that look very ugly, but still serve the same purpose.

Coming back to the problem, as @phischu notes, the capture of a non-bidirectional resume is the union of the capture of the handled statement and the handler bodies. In our paper we just use C for both the statement and for the body, as these are the same region:

@phischu's observation is right in that with

resume { {y} =>
  y.yield()
  e.escape()
}

the handled statement now suddenly not only captures {b,y}, but by running the extended computation, it also captures {e}.

This is indeed an oversight on my part, I am sorry!

It seems like the right thing to do is indeed to require that e is now also part of the capture of resume, which now has a capture of {b,y,e}. I do not know how to implement this most elegantly, at the moment, though.

However, wouldn't this also rule out the following variation?

effect escape(): Nothing
effect yield(): Unit
effect bi{y: yield}: Unit

def main() at {}: Unit = {
  val f =
    try {
      b.bi{y}
      box {}
    }
    with b: bi {
      try {
        resume { {y} =>
          y.yield()
          e.escape()
        }
      } with e: escape { box {} }
    }
    // Here I am immediately calling `resume`, which seems fine, 
    // but would work since it now has capture `{b, e, y}`.
    // However, `e` is not in scope here.
    with y: yield { resume(()) }
  f()
}

[b-studios]

It also seems this is related to handling multiple effects in the same handler, which corresponds to two different shifts that share the same prompt. It is much harder to construct this kind of situation under the restriction that every try only handles one effect.

I retract: Two different shifts over the same prompt, i.e.,

reset { p1 =>
  ...
  shift(p1) { k => ... reset { p2 => resume(k) { ... p2 ... } } }
  ...
  shift(p1) { k => box { resume(k) { return 42 } }
  ...
}

shouldn't be structurally different from one shift with multiple resumes

reset { p1 =>
  ...
  shift(p1) { k => 
    ... reset { p2 => resume(k) { ... p2 ... } }
    ... box { resume(k) { return 42 } }
  }
  ...
}

which is what @kyay10 tried to construct above.

[b-studios]

Soooo, I thought about it for a few minutes now and came to the following conclusion (just rephrasing things already said in this issue):

Bidirectional resumes (resume { stmt }) allow us to send computation s back to callsite of an effect. That is, conceptually computation stmt is now not run in the handler body (the call site of resume), but at the call site of the effect operation.

The example provided by @kyay10 shows that we can have different callsites of resume (one with an additional handler and one without). So we cannot know that the lexical capabilities are actually in scope at all resumes.

My new proposal is thus to forbid closing over any capabilities in the block passed to resume. Sadly, typing-wise this is in essence the same as saying:

resume(box { {y} => ... })

which is very restrictive. However, it is safe :)

[kyay10]

forbid closing over any capabilities in the block passed to resume.

Except for capabilities that resume already captures, right? So that one can use outer handlers inside resume just fine. It'd be nice to also add #1180 in one go here.

I do agree with your assessment here (which corresponds to mode (1) above). There is an alternative (mode (2) above) where we view resume as a block parameter itself, so that it can't be used outside shift's body. That would guarantee that the call-site is permanently changed (I'm handwaving a bit here, but you can convince yourself that if resume must be used inside its shift, then any middle handlers are guaranteed to be preserved).

I'm happy with just going with (1); it is restrictive, but it feels rather natural (and makes a ton of sense in an intermediary calculus that has shift/reset but still tracks captures).

It'd be interesting to see how many pre-existing Effekt programs are ruled out by (1), and what the workarounds look like. I linked and quoted above one of your examples that allocated local mutable state and leaked it into resume (which was fine because your code was valid under mode (2)). The workaround for that case is to use a region. It'd be interesting to see what programs don't have such workarounds. I think a lot of them can be mechanically transformed, actually...

Some thoughts about what a mechanical transformation could look like, potentially showing no loss in expressivity

There's a vague local transformation in my mind that can turn any middle handlers into outer handlers, thus accepting programs that are valid under (1) or (2).

The idea is to "pull out the reset" from inside the shift, and shifts to that reset should add the "continuation" after the reset (I'm not sure exactly what notion of contiunation I'm appealing to here, but I mean that if you have shift { k => e(reset { e2 }) } then e is the continuation). The transformation might roughly look like:

reset { p1 =>
  ...
  p1.shift { k =>
    ...
    e(reset { p2 => e2 })
  }
}

to

reset { p2 =>
  reset { p1 =>
    ...
    p1.shift { k =>
      ...
      e(<REPLACE p2, e, e2>)
    }
  }
}

where <REPLACE p, c, e> means to replace any instances of p.shift { k => e2 } inside e with p.shift { k => c(e2) } This effectively makes the middle handler show up in captures, and so it can't be escaped anymore. Obviously, this is no proof. I've likely missed some corner cases, too. For one, in the case of multiple middle handlers, I think you just need to apply this multiple times, peeling away an inner reset each time.

You can do this manually. It's a little annoying to write this back in effect/handler terms (I wish Effekt had shift/reset support that works well with captures and outer handlers, instead of having to box thunks around to please the capture checker), but it's doable. Because this is local (it's "macro expressible", if you will), I conjecture that Effekt remains just as expressive even with the restrictions imposed by (1).

[kyay10]

Out of curiosity, doesn't Effekt have proofs of effect safety and such? I haven't looked thru some of papers in a while, but I'm guessing the combination of bidirectional effects with boxing wasn't formalized? To be very clear, I don't mean this like "how dare you not have all the proofs!" but more like "huh, I guess one of these extensions wasn't proven correct".

[b-studios]

No, sadly not. The written Effekt saga so far was only "no first class functions (OOPSLA 2020)" -> "first-class functions are back through boxes (OOPSLA 2022)" and then a lot of papers on implementation strategies, but not a lot about objects, bidirectional effects, or their interaction with first class functions.

AFAIK the only publication describing some kind of bidirectional effect handlers is this one: https://dl.acm.org/doi/abs/10.1145/3428207

We are currently in the process of formalizing a new version of our core calculus with bidirectional control-flow and first-class functions, but still not full source Effekt.

[b-studios]

Here is an alternative proposal in three steps:

1. make resume a keyword (NOT a block parameter at all, so it is not even second class)
2. check syntactically, whether resume occurs under a box
3. depending on (2) change the way resume { ... } is type-checked

Details

The first step would be to prevent resume from passively being passed around, such as f(resume), or being stored like def k = resume. This can be achieved by turning it into a keyword and requiring it to be fully applied. If users ever want to pass it, they would need to eta-expand by hand (for now). This has the advantage, that we syntactically can see ALL call-sites.

The second step is to check whether there exists at least one callsite of resume that is under a box (we need a good name for this), since this is where resume could potentially leave the immediately surrounding scope that contains the intermediate ("local") handlers.

The third step is to flip a switch in the type checker based on the result of (2):

• if (2) holds, then the continuation could leave the scope and it must not close over any local capabilities (implement what I proposed above).
• if (2) does not hold, then it is fine to close over it (for instance if we only ever immediately call resume) -- this means we keep typechecking the resumes as we do now.

@kyay10 do you think such as scheme would fix the issues you discovered? I think it is the most flexible solution, so far, while staying somewhat implementable.

[kyay10]

Is this considered fully eta-expanded?

def res() = resume(())

because one can then box res, and I don't see how you'd track that easily. Similarly, this is allowed:

def myBox{block: () => Unit} = box block

myBox { resume(()) }

So maybe the play is to track captures of resume, and when it needs to be "upcasted", that's when to flip the switch? Or maybe just any non-local use of resume immediately flips the switch. So (2) only holds if resume is used very trivially. However, I think this would even rule out using a middle handler that's provided by a def:

def provideFoo{block: {Foo} => Unit} = <>

provideFoo {
  resume { } // error because it's not used locally trivially
}

So this "trivial uses" approach is awfully restrictive.

[b-studios]

Yes you are right, the moment where resume is used under an abstraction (inside of a def, or block parameter), we do not actually know the call-site and could leak it transitively via the def or block parameter. But also just giving up in this situation is also quite restrictive.

Of course one could (as you also suggested above) switch between (1) treating resume as a tracked parameter (which we did in the very first version of Effekt) but allowing captured capabilities and (2) not allowing any captures but treating it as a first-class value.

The most naive version would be to just try (1) and if that fails, fall back to (2). However, this seems awfully wasteful and unprincipled.

[kyay10]

A mildly less naive version is:

• Check all bidirectional resumes first (before any other type checking for resume)
• if any of them capture a middle handler, typecheck using (2)
• otherwise, typecheck using (1)

In other words, expressions involving resume will be typechecked later than other expressions.

Only issue I can foresee is that someone might write code for (2) that boxes a resume or stores it in a def and then uses it while capturing a middle handler. I think it's fair to simply disallow this case, with the very simple workaround being that you must use resume in mode (2) at least once in a way that captures a middle handler (someone can do someting as simple as def myResume{block: {SomeEffect} => SomeType} = resume {block} to get it working). In some sense, this is like your idea of requiring eta-expansions for resume, but less restrictive since it only operates in mode (2) and only requires a single eta-expanded resume to "get the hint".