Type unsoundness in `Control` / coroutine effect interface

[ymdryo]

Hi!

While experimenting with resuming a continuation outside its handler (a.k.a. non‑scoped resumption), I noticed an unsoundness in the coroutine effect.

The code below is well‑typed under the current public Turbolift API, but because the second R.ask goes unhandled, it's invalid from an algebraic-effects standpoint, and in fact triggers a runtime error.

//> using scala "3.7.0"
//> using dep "io.github.marcinzh:turbolift-core_3:0.114.0"

import turbolift.effects._
import turbolift.!!

case object C extends CoroutineEffect[Unit, Unit, (Int, Int)]
type C = C.type

case object R extends Reader[Int]
type R = R.type

val prog: (Int, Int) !! (C & R) = for {
    x <- R.ask
    _ <- C.yeld(())
    y <- R.ask
} yield (x, y)

val step = prog.handleWith(C.handler[Any]).handleWith(R.handler(1)).run

step match
    case CoroutineEffect.Step.Yield((), k) => {
        val step2: CoroutineEffect.Step[Unit, Unit, (Int, Int), C] =
            k(()).handleWith(C.handler).run
    }
    case CoroutineEffect.Step.Exit(_) => println("unreachable")

Exception in thread "main" java.lang.RuntimeException: Fiber failed.
        at scala.sys.package$.error(package.scala:27)
        at turbolift.io.Outcome.get(Outcome.scala:24)
        at turbolift.Computation$.run(Computation.scala:303)
        at tltest$_.<init>(tltest.sc:24)
        at tltest_sc$.script$lzyINIT1(tltest.sc:41)
        at tltest_sc$.script(tltest.sc:41)
        at tltest_sc$.main(tltest.sc:45)
        at tltest_sc.main(tltest.sc)

It works correctly when the correct set of unhandled effects is specified. In this case, it's R, not Any.

val step = prog.handleWith(C.handler[R]).handleWith(R.handler(1)).run

step match
    case CoroutineEffect.Step.Yield((), k) => {
        val step2: CoroutineEffect.Step[Unit, Unit, (Int, Int), C] =
            k(()).handleWith(C.handler).handleWith(R.handler(2)).run
        println(step2) // Exit((1,2))
    }
    case CoroutineEffect.Step.Exit(_) => println("unreachable")

It looks like the coroutine effect handler itself is implemented (and, I believe, ought to be implementable) safely using only the public Control effect interface. Therefore, the root issue appears to lie in an unsoundness in Control. I suspect it's either capture0 or strip, and I think that when it's executed, the set of unhandled effects must be tracked at the type level. I'm still not very familiar with Turbolift (Ambient and the like), so please forgive me if I've gotten anything wrong.

(For some background: I'm also building my own effect system, and when I tried to implement capture0 in a type-safe way, I found I needed to track the list of prompt frames at the type level. If I erase that information, the kind of unsoundness we're seeing here appears; but if I do track it, the type parameters become overly verbose, which has been quite a headache.)

[marcinzh]

Hello! And welcome to the community of Scala programmers!

This is an initial, quick response, before I get deeper into the problem.

Some changes to the code:

• I updated to Turbolift v0.116.0 to disable scala-cli nagging. As a consequence, this requires changing extends Reader to extends ReaderEffect (breaking change in the last release).

• I changed .run to .runIO (used to be named .unsafeRun). This allows us to see the error:

  Failure(Thrown(turbolift.data.Exceptions$Panic: Signature R not found))

  This tells us that the Turbolift's main interpreter loop hasn't found the R effect's prompt on the stack, while trying to execute some operation of R effect.

• I tried an alternative way of using the coroutine, using turbolift.io.Coroutine object. This is an utility construct, that is essentially a wrapper over a mutable reference to the last Step. It also encapsulates a Coroutine effect instance (the fx parameter) for convenience. So, this version turned out to be working. Interesting.

//> using scala "3.7.0"
//> using dep "io.github.marcinzh:turbolift-core_3:0.116.0"
import turbolift.effects._
import turbolift.!!
import turbolift.io._

case object C extends CoroutineEffect[Unit, Unit, (Int, Int)]
type C = C.type

case object R extends ReaderEffect[Int]
type R = R.type

val prog: (Int, Int) !! (C & R) = for {
    x <- R.ask
    _ <- C.yeld(())
    y <- R.ask
} yield (x, y)


def original =
    val step = prog.handleWith(C.handler[Any]).handleWith(R.handler(1)).run

    step match
        case CoroutineEffect.Step.Yield((), k) => {
            // val step2: CoroutineEffect.Step[Unit, Unit, (Int, Int), C] =
            println:
                k(()).handleWith(C.handler).runIO
        }
        case CoroutineEffect.Step.Exit(_) => println("unreachable")


def alternative =
    (for
        coro <- Coroutine.create[Unit, (Int, Int), R]: fx =>
            for
                x <- R.ask
                _ <- fx.yeld(())
                y <- R.ask
            yield (x, y)        
        a <- coro.resume
        b <- coro.resume
    yield (a, b))
    .handleWith(R.handler(1))
    .tapEff(x => Console.println(x.toString))
    .handleWith(Console.handler)
    .runIO


@main def main =
    original
    // alternative

Initial diagnosis:

Looks like CoroutineEffect.handler is wrongly typed:

https://github.com/marcinzh/turbolift/blob/master/modules/core/src/main/scala/turbolift/effects/Coroutine.scala#L32-L34

The U parameter, meaning effect set used in the body of coroutine (besides the CoroutineEffcet itself), is underutilized. I'm thinking now it should be passed downstream as the dependency of the handler. Instead, the handler uses Any (empty set, meaning no dependencies).

You may be right that Control API is unsound, because it allowed this dependency to disappear.

I also need to investigate this part:

    val step = prog.handleWith(C.handler[Any]).handleWith(R.handler(1)).run

Logically, instead of [Any] it should be [R]. Usually the compiler can infer the correct type.

In next post I'll explain what's about the Ambient and Control.strip.

[ultralightspeed]

Hi, could I get a window-level peak into your perspectives on what fascinates you with -> for marcinzh, since this is your library, non‑scoped resumptions and, for you ymdryo, multi-shot continuations since studying heftia is how I ended up here. Noob coming for you reasoning traces plz

[ymdryo]

@ultralightspeed

(It might be better to spin this off into a new discussion)

A multi‑shot continuation is the mechanism you need to implement the Choice effect (also called the non-determinism effect). With it, you can write Prolog‑style code such as logic solvers, search procedures, and back‑tracking that cooperates cleanly with other effects.

Non‑scoped resumption is also an extremely niche term, so let me spell it out. A continuation is like a debugger breakpoint: you first capture one with something like val k = getBreakPoint(), then later call resume(k), and execution jumps back to where the breakpoint was captured, a type‑safe goto if you will. Normally continuations are accessible only inside the implementation of an effect handler, but non‑scoped resumption exposes them to the user of the effect, letting the user craft their own control structures. That extra freedom makes the feature very powerful, and correspondingly hard to implement correctly. This issue is about that difficulty.

[marcinzh]

Hello @ultralightspeed!

I created a new discussion where I answered your question: https://github.com/marcinzh/turbolift/discussions/53

@ymdryo:

There is a part in the above that you might find interesting:

data.data.Stream.uncons s =
  handle s() with cases
    { r }             -> Left r
    { emit hd -> tl } -> Right (hd, (tl : '{g, Stream a} r))

I'm not an Unison expert, but the use of : operator in an expression looks like an explicit type ascription (Scala has it too) applied to the continuation (the tl). I wonder what's in the type of the continuation that required manual help in this case?

[ymdryo]

@marcinzh

Thank you for the investigation!

data.data.Stream.uncons s =
  handle s() with cases
    { r }             -> Left r
    { emit hd -> tl } -> Right (hd, (tl : '{g, Stream a} r))

I'm not an Unison expert, but the use of : operator in an expression looks like an explicit type ascription (Scala has it too) applied to the continuation (the tl). I wonder what's in the type of the continuation that required manual help in this case?

I have not looked into Unison either, so I cannot say for sure, but it certainly looks like the explicit annotation is there because type inference is not sufficient. Assuming Unison has a sound type system, then—just as giving Any instead of R earlier caused trouble—supplying the wrong type such as '{Stream} in place of '{g, Stream} would be rejected at compile time, thus preventing the run-time error.

---

Sorry to jump in before the next reply arrives, but I have found a bit more and would like to share it. I hope this helps your investigation.

What follows seems to be a different, and more fundamental, issue than the coroutine unsoundness shown at the top of the thread.

In short: To implement the Control.delimit primitive soundly, there appears to be an invariant that the prompt-stack environment must not change while code inside the delimit scope is running. That invariant can be violated if a non-scoped resumption occurs inside the delimit scope and switches handlers, thereby mutating the prompt-stack environment. In other words, Control.delimit and non-scoped resumption are in tension; there may be a principled incompatibility between them.

---

(However, I have not thoroughly read Turbolift's internals, and the idea above comes from experiments in Haskell with a multi-prompt control monad and an experimental Control.delimit implementation; I am inferring that Turbolift is based on a similar mechanism, so I might be mistaken. Nevertheless, from what I have seen while playing with Turbolift, its API and behavior look consistent with the mechanism I have in mind. Recently I have been trying a somewhat unusual experiment: implementing an effect monad that is completely well-typed, with no type erasure or unsafe casts, so that no run-time error is possible. When I encounter type errors that simply refuse to go away, they often signal that something unsound is lurking. The examples discussed here were discovered in that manner.)

I have prepared a demo. In this example

• catchToOption is used to demonstrate Control.delimit
• C.yeld is used to switch the prompt-stack environment

The point of variation is the To type (the interpreter's output) of the MaybeEffect handler. At first the To type is Option2; halfway through we switch it to a new type Option.

catchToOption is handled by the initial M.handler2, so the type system believes To = Option2 is fixed there in the delimit scope. However, a non-scoped resumption later replaces the MaybeEffect frame with M.handler, meaning To = Option, and the type system never notices. Thus the code compiles with no type errors, but at runtime the value that was supposed to be an Option2 has been swapped for an Option, leading to a ClassCastException.

//> using scala "3.7.0"
//> using dep "io.github.marcinzh:turbolift-core_3:0.116.0"
import turbolift.effects._
import turbolift.{!!}
import turbolift.Extensions._

case object C extends CoroutineEffect[Unit, Unit, Option[Unit]]
type C = C.type

case object M extends MaybeEffect
type M = M.type

enum Option2[+T]:
    case Some2(x: T)
    case None2

def fromOption2[A](o: Option2[A]) =
    o match
        case Option2.Some2(x) => Some(x)
        case Option2.None2    => None

extension (fx: MaybeEffect)
    def handler2 =
        new fx.impl.Stateless[Identity, Option2, Any]
            with fx.impl.Sequential
            with MaybeSignature:
            override def onReturn(a: Unknown) = !!.pure(Option2.Some2(a))
            override def empty = Control.abort(Option2.None2)
            override def catchToOption[A, U <: ThisEffect](body: A !! U) =
                Control.delimit(body).map(fromOption2)
        .toHandler

val prog = M.catchToOption:
    for {
        _ <- C.yeld(())
        _ <- M.empty
    } yield ()

val step1 = prog
    .handleWith(C.handler[M])
    .handleWith(M.handler2)
    .run

step1 match
    case Option2.Some2(CoroutineEffect.Step.Yield((), k)) => {
        val step2 =
            k(()).handleWith(C.handler[M]).handleWith(M.handler).run
        step2 match
            case Some(x) =>
                x match
                    case CoroutineEffect.Step
                            .Exit(result) => {} // runtime error occurs here
                    case _ => println("unreachable")
            case _ => println("unreachable")
    }
    case _ => println("unreachable")

Exception in thread "main" java.lang.ClassCastException: class tltest$_$$anon$3 cannot be cast to class scala.Option (tltest$_$$anon$3 and scala.Option are in unnamed module of loader 'app')
        at tltest$_.<init>(tltest.sc:52)
        at tltest_sc$.script$lzyINIT1(tltest.sc:71)
        at tltest_sc$.script(tltest.sc:71)
        at tltest_sc$.main(tltest.sc:75)
        at tltest_sc.main(tltest.sc)

---

I do not yet fully understand the cure, but it seems we need a mechanism that prevents (or freezes) changes to the prompt-stack environment while executing inside a delimit scope. This likely corresponds to the semantics of turbolift.io.Coroutine.

• In the orthodox algebraic-effects semantics of non-scoped resumption, the second R.ask runs under a fresh outer environment and therefore returns 2.
• Under the proposed "environment-freezing" semantics, the environment is locked at the moment we enter a prompt scope, so both R.asks return 1.

This means giving up the "algebraic-effects-faithful" semantics for non-scoped resumption, but I think it is an acceptable in practice.

Going forward I plan to provide two library variants in Haskell and let users choose according to their needs:

1. Algebraic-effects faithfulness first

   • Non-scoped resumption keeps the orthodox semantics
   • Control.delimit cannot be used

2. Higher-order-effects convenience first

   • Control.delimit is available, so higher-order effects work without restriction (like CatchFail.hs)
   • Non-scoped resumption follows the environment-freezing semantics

(I expect that almost all users will want option 2.)

If I also uncover anything on my side that might point toward a solution, I'd like to let you know.