I’ve been looking at the code of boundary and have a capture-checking related question.
Label extends Capability, which is perfectly reasonable: it cannot be allowed to escape, otherwise we might end up using it in a call to break outside of the try / catch block that knows to catch it.
This makes Break a little problematic, because of course Break captures the associated Label. Is this why the label field is defined as Label[T]^{}? I’m reading this rather naively and interpreting it as even though Label always has cap in its capture set, this overwrites it to be empty.
Which takes us to creating Break values: again, problematic, because how do you pass an untracked Label to Break, since Label is always tracked? and the code answers this by calling unsafeAssumePure, so is it correct to assume that this drops the capture set even of types who are declared as always having a non-empty capture set like Label?
This unsafe calls has comment:
// SAFETY: labels cannot leak from [[Break]] [...]
Why? Neither Label nor Break are flagged as private, what stops me from manually catching Break, extracting the Label, and returning that?
Are you trying to implement longjmp here?
Why would a nice fellow want to do that? 
Sorry, way above my level, my advice is to leave it alone, maybe it’s an implementation wart?
The reason the label field was left public was because of source compatibility: it was always public. We could swap it with another Break class, but due to inlining I don’t think we can leave the old class as it would always be vulnerable. The original proposal was to mark it private[boundary], and only allow comparison between labels be exposed (which is the purpose of the new sameLabelAs method).
Perhaps a comment should be added to note that extracting the label is unsafe.
Another piece of the puzzle here was from Break being an exception: we enforce Java types to be pure for interoperability, and that includes jl.Exception itself. Therefore it is a constraint on the library design itself to keep Break pure and enforce label-safety purely through scoping.
1 Like
Thanks for that answer, it’s clear and very useful.
Out of curiosity, what was the alternative? Could you have made Break capture its label (assuming compatibility was not an issue)? Break can be made private and an implementation detail that no one could interact with, so arguably, making it pure is not terribly important (again, removing the compatibility constraint for the sake of argument).
I tried that but couldn’t work out make Break capture its label, the compiler error mentions self types and i didn’t really know what to do with that…
For example:
private case class Break[A](label: Label[A], value: A)
extends ControlThrowable with NoStackTrace
Yields:
reference (Break.this.label : Label[A]) is not included in the allowed capture set {} of the self type of class Break
I tried fixing that with the obvious, naive interpretation of the error message:
private case class Break[A](label: Label[A], value: A)
extends ControlThrowable with NoStackTrace:
self: Break[A]^{label} =>
But this then fails with:
Break[A] is a pure type, it makes no sense to add a capture set to it
And I have to admit I’m a little at a loss at what to do at this point.
Unfortunately the error lies already in the extends ControlThrowable, which has a lineage of ControlThrowable <: java.lang.Throwable. At the moment the compiler enforces every Java class (aside from Object itself) to have a pure self-type, i.e. cannot hold any tracked references. So for now that means you cannot throw tracked exceptions…
Oh i see, i hadn’t realised this was enforced by the compiler! Thank you, that clarifies everything.
I’m a little curious though - shouldn’t everything Java be considered impure rather than pure by default? I would assume the decision was for backwards compatibility reasons, but there’s not any backwards compatibility to worry about on capture checking (yet).