effekt-lang / effekt-lang/effekt

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

Open
#1,176 18 comments 4 reactions 1 assignee Claimed by @b-studios View on GitHub
bug
Dominant language
Scala
Stars
469
Forks
41
Avg merge
1d 16h
Merged PRs (30d)
23

Description

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"):
```effekt
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:
```effekt
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)
```effekt
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 receive[Int]())
println(4)
println(do receive[Int]())
} {
println(2)
do send(3)
println(5)
do send(6)
println(7)
}
}
```

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.