Consider the following program:
import language.experimental.captureChecking
import caps.*
class A:
consume def take(): Int = 0
// Functions that can be called only once
trait FnOnce:
consume def apply(): Unit
def f() =
val a: A^ = A()
val consumeFunction: FnOnce^{a} = new FnOnce:
consume def apply() = println(a.take()) // errors here
consumeFunction() // function is consuming a anyway
Here, the compiler rejects the definition of consumeFunction, since it tries to consume a, which is outside of scope.
Separation failure: call prefix of consume method take refers to non-local value a
Note however that it is
- only consumed within a consume method of
consumeFunction, and
- the reference
a is recorded in the capture set of consumeFunction, which is consumed if it was going to be invoked. This means consuming a is sound.
We should indeed allow consuming arbitrary references outside of scopes of consume methods, which should increase expressivity of the system, while seemingly introducing no complications.
In the future, this can be refined (calling a consume method might not consume all references of an object), which might require more from the system (consume qualifiers in capture sets?)
Consider the following program:
Here, the compiler rejects the definition of
consumeFunction, since it tries to consumea, which is outside of scope.Note however that it is
consumeFunction, andais recorded in the capture set ofconsumeFunction, which is consumed if it was going to be invoked. This means consumingais sound.We should indeed allow consuming arbitrary references outside of scopes of
consumemethods, which should increase expressivity of the system, while seemingly introducing no complications.In the future, this can be refined (calling a consume method might not consume all references of an object), which might require more from the system (consume qualifiers in capture sets?)