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.
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.
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).
12
12
13
13
### Existential Binding
14
14
@@ -44,7 +44,7 @@ is interpreted as having an existentially bound `cap` in the result, like this:
44
44
```
45
45
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
46
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 `(A₁, ..., Aₖ) -> B^` don't bind their result cap in an existential quantifier. For instance, the function
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 `(A₁, ..., Aₖ) -> B^` don't bind the `cap` in their return types in an existential quantifier. For instance, the function
48
48
```scala
49
49
(x: A) ->B->C^
50
50
```
@@ -74,8 +74,8 @@ To summarize:
74
74
75
75
## Levels and Escape Prevention
76
76
77
-
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. Later sections on [capability classifiers](classifiers.md) will add a controlled
78
-
escape mechanism.
77
+
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
78
+
where this would be desirable.
79
79
80
80
### How Levels Are Computed
81
81
@@ -153,7 +153,7 @@ called _charging_ the capability to the environment.
153
153
```scala
154
154
defouter(fs: FileSystem^):Unit=
155
155
definner(): () ->{fs} Unit=
156
-
() => fs.read() //cap1 is used here
156
+
() => fs.read() //fs is used here
157
157
inner()
158
158
```
159
159
@@ -173,10 +173,10 @@ The closure is declared pure (`() -> Unit`), meaning its `cap` is the empty set.
173
173
174
174
## Visibility and Widening
175
175
176
-
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 superset:
176
+
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:
177
177
178
178
```scala
179
-
deftest(fs: FileSystem^):Logger^{cap} =
179
+
deftest(fs: FileSystem^):Logger^{fs} =
180
180
vallocalLogger=Logger(fs)
181
181
localLogger // Type widens from Logger^{localLogger} to Logger^{fs}
0 commit comments