The capture checking documentation states the following:
A subcapturing relation C₁ <: C₂ holds if C₂ accounts for every element c in C₁. This means one of the following three conditions must be true:
- […]
- […]
c’s type has capturing set C and C₂ accounts for every element of C (that is, C <: C₂).
While the first 2 rules make intuitive sense, this one is a little less obvious to me. Turning into code, I get the following:
class A
val s: A^ = A()
val s1: A^{s} = A()
val s2: A^{s1} = A()
s2: A^{s}
This all compiles, which is expected given that third rule. But naively, it feels that:
- being able to state
s2: A^{s} means that A^{s1} <: A^{s}
- this, in turns, means
{s1} <: {s}
- (this might be my mistake)
{s1} captures s1, and everything s1 captures: {s1, s}.
- this leads to
{s1, s} <: {s}, which feels wrong: it means I can “shrink” a capture set, potentially loosing the information needed by the typechecker to prevent s1 from escaping.
I would be grateful for an explanation of where I’m wrong, and for the purpose of that third accounting rule!
1 Like
The problem with this example is that A is not a tracked Capability type and hence treated as “pure”. Pure types are compatible with any capturing type.
It’s more interesting if we define class A extends Capability (or use something in its stead that has to be tracked). Then we can only do the following:
class A extends Capability
val s: A^ = A()
val s1: A^{s} = s // A() yields an error
val s2: A^{s1} = s1 // A() yields an error
s2: A^{s}
Subcapturing is not just set inclusion, but also takes into account if some capability is derived from another, which is modeled by the third rule. It accounts for aliasing, which justifies
{s2} <: {s1} <: {s}
and by transitivity
{s2} <: {s}
That should satisfy intuitive expectations, because being aliases of s, we should be able to pass A^{s1} and A^{s2} where A^{s} is expected. Though one should note that subcapturing does not model full aliasing, e.g., the other direction {s} <: {s1} is not derivable (we generally don’t want to pay the price for precise alias tracking).
Now if we have {s1} <: {s} we can also derive (by adding s to both sides)
{s1, s} <: {s, s} = {s}
And that’s ok! {s} definitely subsumes itself and a (transitive) alias for it. By analogy with normal types and union types, if we have T <: U, then we’d expect that T | U <: U.
1 Like
I’m going to have to think hard about that answer 
First, thank you for taking the time to answer. This is currently confusing me more than it’s helping, but that’s because you’re fixing misunderstandings. I really appreciate it.
Your point about A being non-capturing is well made and made me think really hard for a few minutes - wait, is he saying that extends Capability is not simply syntactic sugar for ^{cap}?.
Now I realize you mean A’s constructor returns a pure type and so can be treated as A^{s}. This is fair, but also, kind of not the point I was trying to make
I was not thinking about values at all - not trying to make s2 an alias of s1 or of s, but trying to have “linked” capture sets. s2 captures s1 captures s, regardless of their actual values. And to me, it feels like s2 : A^{s} means I can drop the fact s1 was captured by s2, which bothers me because, maybe mistakenly, I’m seeing capture checking as primarily a tool to prevent undesired escapes, and it feels like s1 might very well escape there.
The way I manage to reconcile that in my head is probably incorrect, but goes something like this:
s2: A^{s1} does not capture cap, which means we’re tracking it because it captures something else we don’t want escaping. Our only candidate is s1.s1: A^{s} does not capture cap either, so we keep looking deeper, to s.s: A^{cap} does capture cap, so s2 is really saying we don’t want s to escape. Which makes it ok to treat A^{s1} as A^{s}.
Is that a more complicated way of saying “s2 aliases s” ?
It’s imo more useful to consider actual examples to understand the point of the subcapturing rules.
The last rule you ask about is for relating name bindings in the context with their assumed types/captures. That way, we can track the lineage of a binding: s2: A^{s1}, could mean s2 is an alias for s1, or it’s a value that closes over s1, or s2 derives authority from s1 to do something, s2 touches s1, etc. Which is to say there are a few useful intuitions on what exactly the binding can mean. But more technically, tracking s2 obligates the compiler to track s1, and looking at s1’s type, it is also obligated to track s, etc.
Values are essential! For example, capture sets of function types reflect the underlying function value/closures free variables/capabilities. It’s values that determine these lineages and the point of the subcapturing rules is to model them (which is why I object to using a non-Capability type, that’s cheating).
We are not dropping this fact here. It just says s2 also captures s (due to its lineage).
I suggest trying a concrete example to see why this is not the case.
See, I think this is the crux of my problem.
Rule 1 states that if C1 ⊆ C2 then C1 <: C2 (where C1 and C2 are capturing sets). This seems reasonable to me: when you use T^C1 where T^C2 is expected, you’re not loosing any tracked variable, merely adding the ones that are in C2 but not C1.
But it seems you’re saying something that’s kind of the opposite: using A^{s1} where A^{s} is expected is ok, because {s1} is “bigger” than {s} - it captures both {s1} and {s}. That’s the bit that really bothers me about rule 3: it feels like a contradiction of rule 1
I manage to make it work in my head by thinking that any value that doesn’t capture cap is not tracked for itself, but merely because it captures things that we care about tracking. I have no idea whether that’s even remotely close to the right intuition.