Open
Description
Compiler version
Latest nightly
Minimized code
With recent support for capture variables, abstract capture members and paths
in and to captures, we can obtain a reasonable signature for boundary/break
or similar delimiter pairs that prevent leaking inner labels,
using path-dependent types:
import language.experimental.captureChecking
import caps.*
trait BoundaryBreak:
trait Label extends Capability:
type Cap >: CapSet <: CapSet^
def boundary[T,C^](block: Label{type Cap = C} ->{C^} T): T = ???
def suspend[U](label: Label)(handler: () ->{label.Cap^} U): U = ???
def test =
val x = 1
boundary: outer =>
val y = 2
boundary: inner =>
val z = 3
suspend(outer): () =>
println(inner) // error , good!
x + y + z
trait File extends Capability:
def write(s: String): Unit
def read(): String
def test2 =
val f1: File = ???
boundary: outer =>
val f2: File = ???
suspend(outer): () =>
f1.write("ynot") // error, but should be legal
Output
In test2
, we get an error:
-- Error: local/boundarybreak.scala:36:8 ---------------------------------------
36 | f1.write("ynot")
| ^^
|reference (f1 : BoundaryBreak.this.File^) is not included in the allowed capture set {outer.Cap^}
|of an enclosing function literal with expected type () ->{outer.Cap^} Unit
but we can make it work by explicitly annotating the expected capture set of the body:
def test3 =
val f1: File = ???
boundary[Unit,CapSet^{f1}]: outer =>
val f2: File = ???
suspend(outer): () =>
f1.write("ynot") // accepted now!
Expectation
Ideally, inference of types/captures would correctly infer CapSet^{f1}