You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When discussing escape checking, we referred to a scoping discipline. That is, capture sets can contain only capabilities that are visible at the point where the set is defined. But that raises the question: where is a universal capability `cap` defined? In fact, what is written as the top type `cap` can mean different capabilities, depending on scope. Usually a `cap` refers to a universal capability defined in the scope where the `cap` appears.
9
+
When discussing [escape checking](basics.md#escape-checking), we referred to a scoping discipline. That is, capture sets can contain only capabilities that are visible at the point where the set is defined. But that raises the question: where is a universal capability `cap` defined? In fact, what is written as the top type `cap` can mean different capabilities, depending on scope.
10
10
11
-
A useful mental model is to think of `cap` as a "container" that can _absorb_ concrete capabilities. When you write `T^` (shorthand for `T^{cap}`), you're saying "this value may capture some capabilities that will flow into this `cap`." Different `cap` instances in different scopes are different containers: a capability that flows into one doesn't automatically flow into another. We will further expand on this idea later when discussing [separation checking](separation-checking.md).
11
+
## Different Kinds of Caps
12
12
13
-
### Existential Binding
13
+
We will discuss three distinct kinds of `cap` in this chapter:
14
14
15
-
Special rules apply to `cap`s in method and function parameters and results. For example, take this method:
15
+
**Local caps**: Every class, method body, and block has its own local `cap`. It abstracts over the capabilities used inside that scope, representing them by a single name to the outside world. Local caps form a subcapturing hierarchy based on lexical nesting.
16
+
17
+
**Parameter caps**: When `cap` appears in a function parameter type (e.g., `def foo(x: T^)`), it gets its own cap scoped to that parameter. At call sites, parameter caps are instantiated to the actual capabilities passed in.
18
+
19
+
**Result caps**: When `cap` appears in a function result type (e.g., `def foo(x: T): U^`), it becomes an existentially-bound cap that describes what the caller receives. Unlike local caps, result caps do _not_ subsume the enclosing scope's `cap`.
20
+
21
+
So, when writing `T^` (shorthand for `T^{cap}`), `cap` is a way of saying "captures something" without
22
+
naming what it is precisely, and depending of the context occurrence of such `cap`s, the capture checker imposes
23
+
restrictions on which capabilities are allowed to flow into them. We will further expand on this idea
24
+
(and other kinds of `cap`) later when discussing [separation checking](separation-checking.md).
25
+
26
+
Another analogy for the different `cap`s is that they are some form of implicitly named existential or abstract self-capture set attached to elements of the program structure, e.g., scopes, parameters, or return values.
27
+
28
+
## Subcapturing and Levels
29
+
30
+
Local `cap`s form a subcapturing hierarchy based on lexical nesting: a nested scope's local `cap` subsumes its enclosing scope's local `cap`. This makes sense because the inner scope can use any capability available in the outer scope
31
+
as well as locally defined ones. At the top level, there is a true universal `cap` — the local `cap` of the global scope — which all other local `cap`s ultimately subsume:
32
+
33
+
```scala
34
+
// top level: the global `cap`
35
+
classOuter:// has local cap₁
36
+
valf1:File^=File("f1") // File^{cap₁}
37
+
defmethod() =// has local cap₂
38
+
valf2:File^=File("f2") // File^{cap₂}
39
+
varref: () =>Unit=null// () ->{cap₂} Unit, can accept what can flow into cap₂
40
+
valclosure= () =>// has local cap₃
41
+
valf3:File^=File("f3") // File^{cap₃}
42
+
valf4:File^= f2 // ok, because {cap₂} <: {cap₃}
43
+
valf5:File^= f1 // ok, because {cap₁} <: {cap₃}
44
+
ref = () => f3.read() // error, f3 is at the level of cap₃ and cannot flow into cap₂
45
+
...
46
+
```
47
+
48
+
Each capability has a _level_ corresponding to the local `cap` of its defining scope. The level determines where a capability can flow: it can flow into `cap`s at the same level or more deeply nested, but not outward to enclosing scopes (which would mean a capability lives longer than its lexical lifetime). The compiler computes a capability's level by walking up the ownership chain until reaching a symbol that represents a level boundary. Level boundaries are:
49
+
-**Classes** (but not inner non-static module classes)
50
+
-**Methods** (but not accessors or constructors)
51
+
52
+
Local values like `f1`, `f2`, `ref`, etc., don't define their own levels. They inherit the level of their enclosing method or class. For example, this means:
53
+
-`f1` is at `Outer`'s level, i.e., `f` subcaptures local `cap₁`.
54
+
-`f2` and `ref` are both at `method`'s level, i.e., both subcapture local `cap₂`.
55
+
- By lexical lifetime, `{cap₂} <: {cap₃}` holds, but it does **not** hold that `{cap₃} <: {cap₂}`. Hence,
56
+
we cannot assign the closure to `ref`, because `{f3}` is subcapture-bounded by `{cap₃}`.
57
+
58
+
### Charging Captures
59
+
60
+
When a capability is used, it must be checked for compatibility with the capture-set constraints of all enclosing scopes. This process is called _charging_ the capability to the environment.
61
+
62
+
```scala
63
+
defouter(fs: FileSystem^):Unit=
64
+
definner(): () ->{fs} Unit=
65
+
() => fs.read() // fs is used here
66
+
inner()
67
+
```
68
+
69
+
When the capture checker sees `fs.read()`, it verifies that `fs` can flow into each enclosing scope:
70
+
1. The immediately enclosing closure `() => fs.read()` must permit `fs` in its capture set ✓
71
+
2. The enclosing method `inner` must account for `fs` (it does, via its capture set) ✓
72
+
3. The enclosing method `outer` must account for `fs` (it does, via its parameter) ✓
73
+
74
+
If any scope refuses to absorb the capability, capture checking fails:
The closure is declared pure (`() -> Unit`), meaning its local cap is the empty set. The capability `fs` cannot flow into an empty set, so the checker rejects this.
82
+
83
+
### Visibility and Widening
84
+
85
+
When capabilities flow outward to enclosing scopes, they must remain visible. A local capability cannot appear in a type outside its defining scope. In such cases, the capture set is _widened_ to the smallest visible super capture set:
86
+
87
+
```scala
88
+
deftest(fs: FileSystem^):Logger^=
89
+
vallocalLogger=Logger(fs)
90
+
localLogger // Type widens from Logger^{localLogger} to Logger^{fs}
91
+
```
92
+
93
+
Here, `localLogger` cannot appear in the result type because it's a local variable. The capture set `{localLogger}` widens to `{fs}`, which covers it (since `localLogger` captures `fs`) and is visible outside `test`. In effect, `fs` flows into the result's cap instead of `localLogger`.
94
+
95
+
## Existential Binding in Function Types
96
+
97
+
So far we've discussed local `cap`s that follow the lexical nesting hierarchy. But `cap` can also appear in function parameter and result types, where special binding rules apply.
There's a connection with [capture polymorphism](polymorphism.md) here. `cap`s in function parameters behave like additional capture parameters that can be instantiated at the call site to arbitrary capabilities.
34
120
35
-
### Function Types
121
+
### Why Result Caps Don't Subcapture Local Caps
122
+
123
+
Result `cap`s do _not_ subsume the enclosing scope's local `cap`. Result `cap`s are bound at the function boundary, not within the function body:
124
+
125
+
```scala
126
+
defouter(): () ->File^=
127
+
vallocalFile:File^= openFile()
128
+
() => localFile // Error!
129
+
```
130
+
131
+
The return type `() -> File^` contains an existentially-bound result cap. If this result cap subcaptured `outer`'s local cap, then `localFile` could flow into it, and the local file would escape. The whole point of the existential is to describe what the _caller_ receives — it must not allow capabilities from the callee's scope to leak out.
132
+
133
+
In contrast, a local cap inside a function body _does_ subcapture the enclosing local cap:
134
+
135
+
```scala
136
+
defouter():Unit=
137
+
valf:File^= openFile() // This ^ is outer's local cap
138
+
valg: () =>Unit= () => f.read() // OK: closure's local cap subcaptures outer's local cap
139
+
```
140
+
141
+
Here the closure's local cap can absorb `f` because both are nested within `outer`.
142
+
143
+
### Expansion Rules for Function Types
36
144
37
145
The conventions for method types carry over to function types. A dependent function type
38
146
```scala
@@ -44,8 +152,7 @@ is interpreted as having an existentially bound `cap` in the result, like this:
44
152
```
45
153
The same rules hold for the other kinds of function arrows, `=>`, `?->`, and `?=>`. So `cap` can in this case absorb the function parameter `x` since `x` is locally bound in the function result.
46
154
47
-
However, the expansion of `cap` into an existentially bound variable only applies to functions that use the dependent function style syntax, with explicitly named parameters. Parametric functions such as `A => B^` or
48
-
`(A₁, ..., Aₖ) -> B^` don't bind the `cap` in their return types in an existential quantifier. For instance, the function
155
+
However, the expansion of `cap` into an existentially bound variable only applies to functions that use the dependent function style syntax, with explicitly named parameters. Parametric functions such as `A => B^` or `(A₁, ..., Aₖ) -> B^` don't bind the `cap` in their return types in an existential quantifier. For instance, the function
49
156
```scala
50
157
(x: A) ->B->C^
51
158
```
@@ -73,56 +180,11 @@ To summarize:
73
180
- Occurrences of `cap` elsewhere are not translated. They can be seen as representing an existential in the
74
181
scope of the definition in which they appear.
75
182
76
-
## Levels and Escape Prevention
77
-
78
-
Each capability has a _level_ corresponding to where it was defined. The level determines where a capability can flow: it can flow into `cap`s at the same level or more deeply nested, but not outward to enclosing scopes (which would mean a capability lives longer than its lexical lifetime). Later sections on [capability classifiers](classifiers.md) will add a controlled mechanism that permits escaping/flowing outward for situations
79
-
where this would be desirable.
80
-
81
-
### How Levels Are Computed
82
-
83
-
A capability's level is determined by its _level owner_, which the compiler computes by walking up the ownership chain until reaching a symbol that represents a level boundary. Level boundaries are:
84
-
-**Classes** (but not inner non-static module classes)
85
-
-**Methods** (but not accessors or constructors)
86
-
87
-
Consider this example:
183
+
Later sections on [capability classifiers](classifiers.md) will add a controlled mechanism that permits capabilities to escape their level for situations where this would be desirable.
88
184
89
-
```scala
90
-
defouter(c1: Cap^) =// level: outer
91
-
valx=1// level: outer (vals don't create levels)
92
-
varref: () =>Unit= () => ()
93
-
94
-
definner(c2: Cap^) =// level: inner
95
-
valy=2// level: inner
96
-
valf= () => c2.use()
97
-
ref = f // Error: c2 would escape its level
98
-
99
-
classLocal:// level: Local
100
-
defmethod(c3: Cap^) =// level: method
101
-
valz= c3 // level: method
102
-
```
103
-
104
-
Local values like `x`, `y`, and `z` don't define their own levels. They inherit the level of their enclosing method or class. This means:
105
-
-`c1` and `ref` are both at `outer`'s level
106
-
-`c2` and `f` are both at `inner`'s level
107
-
-`c3` and `z` are both at `method`'s level
108
-
109
-
### The Level Check
110
-
111
-
A capability can flow into a `cap` only if that `cap`'s scope is _contained in_ the capability's level owner. In the example above, `ref.set(f)` fails because:
112
-
-`ref`'s type parameter has a `cap` that was instantiated at `outer`'s level
113
-
-`f` captures `c2`, which is at `inner`'s level
114
-
-`outer` is not contained in `inner`, so `c2` cannot flow into `ref`'s `cap`
115
-
116
-
This ensures capabilities flow "inward" to more nested scopes, never "outward" to enclosing ones.
117
-
118
-
### Comparison with Rust Lifetimes
185
+
## Comparison with Rust Lifetimes
119
186
120
-
Readers familiar with Rust may notice similarities to lifetime checking. Both systems prevent
121
-
references from escaping their valid scope. In Rust, a reference type `&'a T` carries an explicit
122
-
lifetime parameter `'a`. In Scala's capture checking, the lifetime is folded into the capability
123
-
name itself: `T^{x}` says "a `T` capturing `x`," and `x`'s level implicitly determines how long this
124
-
reference is valid. A capture set then acts as an upper bound on the lifetimes of all the
125
-
capabilities it contains.
187
+
Readers familiar with Rust may notice similarities to lifetime checking. Both systems prevent references from escaping their valid scope. In Rust, a reference type `&'a T` carries an explicit lifetime parameter `'a`. In Scala's capture checking, the lifetime is folded into the capability name itself: `T^{x}` says "a `T` capturing `x`," and `x`'s level implicitly determines how long this reference is valid. A capture set then acts as an upper bound on the lifetimes of all the capabilities it contains.
126
188
127
189
Consider a `withFile` pattern that ensures a file handle doesn't escape:
128
190
@@ -162,46 +224,9 @@ In both cases, the type system prevents the handle from escaping the callback. R
162
224
The key analogies are:
163
225
-**Capability name ≈ Lifetime parameter**: Where Rust writes `&'a T`, Scala writes `T^{x}`. The capability `x` carries its lifetime implicitly via its level.
164
226
-**Capture set ≈ Lifetime bound**: A capture set `{x, y}` bounds the lifetime of a value to be no longer than the shortest-lived capability it contains.
165
-
-**Level containment ≈ Outlives**: Rust's `'a: 'b` (a outlives b) corresponds to Scala's level check (inner scopes are contained in outer ones).
227
+
-**Level containment ≈ Outlives**: Rust's `'a: 'b` (a outlives b) corresponds to Scala's level check (outer scopes can
-**Explicit vs. implicit**: Rust lifetimes are explicit parameters (`&'a T`). Scala levels are computed automatically from program structure: you name the capability, not the lifetime.
170
-
171
-
## Charging Captures to Enclosing Scopes
172
-
173
-
When a capability is used, it must be checked for compatibility with the capture-set constraints of
174
-
all enclosing scopes. This process is called _charging_ the capability to the environment.
175
-
176
-
```scala
177
-
defouter(fs: FileSystem^):Unit=
178
-
definner(): () ->{fs} Unit=
179
-
() => fs.read() // fs is used here
180
-
inner()
181
-
```
182
-
183
-
When the capture checker sees `fs.read()`, it verifies that `fs` can flow into each enclosing scope:
184
-
1. The immediately enclosing closure `() => fs.read()` must permit `fs` in its capture set ✓
185
-
2. The enclosing method `inner` must account for `fs` (it does, via its result type) ✓
186
-
3. The enclosing method `outer` must account for `fs` (it does, via its parameter) ✓
187
-
188
-
If any scope refuses to absorb the capability, capture checking fails:
The closure is declared pure (`() -> Unit`), meaning its `cap` is the empty set. The capability `fs` cannot flow into an empty set, so this is rejected.
196
-
197
-
### Visibility and Widening
198
-
199
-
When capabilities flow outward to enclosing scopes, they must remain visible. A local capability cannot appear in a type outside its defining scope. In such cases, the capture set is _widened_ to the smallest visible super capture set:
200
-
201
-
```scala
202
-
deftest(fs: FileSystem^):Logger^=
203
-
vallocalLogger=Logger(fs)
204
-
localLogger // Type widens from Logger^{localLogger} to Logger^{fs}
205
-
```
206
-
207
-
Here, `localLogger` cannot appear in the result type because it's a local variable. The capture set `{localLogger}` widens to `{fs}`, which covers it (since `localLogger` captures `fs`) and is visible outside `test`. In effect, `fs` flows into the result's `cap` instead of `localLogger`.
232
+
-**Explicit vs. implicit**: Rust lifetimes are explicit parameters (`&'a T`). Scala levels are computed automatically from program structure: you name the capability, not the lifetime.
0 commit comments