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
Better printing of capabilities in error messages (#23701)
- Special case in some situations so that we only print the name,
not the underlying type.
- Print TermParamRefs like other singleton types
- Use unique names to print empty capture set variables
Copy file name to clipboardExpand all lines: docs/_docs/reference/experimental/cc.md
+36-51Lines changed: 36 additions & 51 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -44,9 +44,11 @@ followed by `^`. We'll see that this turns the parameter into a _capability_ who
44
44
If we now try to define the problematic value `later`, we get a static error:
45
45
```
46
46
| val later = usingLogFile { f => () => f.write(0) }
47
-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
48
-
|The expression's type () => Unit is not allowed to capture the root capability `cap`.
49
-
|This usually means that a capability persists longer than its allowed lifetime.
47
+
| ^^^^^^^^^^^^^^^^^^^^^^^^^
48
+
| Found: (f: java.io.FileOutputStream^'s1) ->'s2 () ->{f} Unit
49
+
| Required: java.io.FileOutputStream^ => () ->'s3 Unit
50
+
|
51
+
| Note that capability f cannot be included in outer capture set 's3.
50
52
```
51
53
In this case, it was easy to see that the `logFile` capability escapes in the closure passed to `usingLogFile`. But capture checking also works for more complex cases.
52
54
For instance, capture checking is able to distinguish between the following safe code:
@@ -58,11 +60,11 @@ val xs = usingLogFile { f =>
58
60
and the following unsafe one:
59
61
```scala
60
62
valxs= usingLogFile { f =>
61
-
LazyList(1, 2, 3).map { x => f.write(x); x * x }
63
+
LzyList(1, 2, 3).map { x => f.write(x); x * x }
62
64
}
63
65
```
64
66
An error would be issued in the second case, but not the first one (this assumes a capture-aware
65
-
formulation of `LazyList` which we will present later in this page).
67
+
formulation `LzyList` of lazily evaluated lists, which we will present later in this page).
66
68
67
69
It turns out that capture checking has very broad applications. Besides the various
68
70
try-with-resources patterns, it can also be a key part to the solutions of many other long standing problems in programming languages. Among them:
@@ -87,12 +89,12 @@ The capture checker extension introduces a new kind of types and it enforces som
87
89
Capture checking is done in terms of _capturing types_ of the form
88
90
`T^{c₁, ..., cᵢ}`. Here `T` is a type, and `{c₁, ..., cᵢ}` is a _capture set_ consisting of references to capabilities `c₁, ..., cᵢ`.
89
91
90
-
A _capability_ is syntactically a method- or class-parameter, a local variable, or the `this` of an enclosing class. The type of a capability
92
+
An _object capability_ is syntactically a method- or class-parameter, a local variable, or the `this` of an enclosing class. The type of a capability
91
93
must be a capturing type with a non-empty capture set. We also say that
92
94
variables that are capabilities are _tracked_.
93
95
94
96
In a sense, every
95
-
capability gets its authority from some other, more sweeping capability which it captures. The most sweeping capability, from which ultimately all others are derived is written `cap`. We call it the _universal capability_.
97
+
capability gets its authority from some other, more sweeping capability which it captures. The recursion stops with a _universal capability_, written `cap`, from which all other capabilities are ultimately derived.
96
98
If `T` is a type, then `T^` is a shorthand for `T^{cap}`, meaning `T` can capture arbitrary capabilities.
97
99
98
100
Here is an example:
@@ -105,8 +107,8 @@ class Logger(fs: FileSystem^):
105
107
deftest(fs: FileSystem^) =
106
108
vall:Logger^{fs} =Logger(fs)
107
109
l.log("hello world!")
108
-
valxs:LazyList[Int]^{l} =
109
-
LazyList.from(1)
110
+
valxs:LzyList[Int]^{l} =
111
+
LzyList.from(1)
110
112
.map { i =>
111
113
l.log(s"computing elem # $i")
112
114
i * i
@@ -118,9 +120,9 @@ and retained as a field in class `Logger`. Hence, the local variable `l` has typ
118
120
`Logger^{fs}`: it is a `Logger` which retains the `fs` capability.
119
121
120
122
The second variable defined in `test` is `xs`, a lazy list that is obtained from
121
-
`LazyList.from(1)` by logging and mapping consecutive numbers. Since the list is lazy,
123
+
`LzyList.from(1)` by logging and mapping consecutive numbers. Since the list is lazy,
122
124
it needs to retain the reference to the logger `l` for its computations. Hence, the
123
-
type of the list is `LazyList[Int]^{l}`. On the other hand, since `xs` only logs but does
125
+
type of the list is `LzyList[Int]^{l}`. On the other hand, since `xs` only logs but does
124
126
not do other file operations, it retains the `fs` capability only indirectly. That's why
125
127
`fs` does not show up in the capture set of `xs`.
126
128
@@ -138,7 +140,7 @@ This type is a shorthand for `(A -> B)^{c, d}`, i.e. the function type `A -> B`
138
140
The impure function type `A => B` is treated as an alias for `A ->{cap} B`. That is, impure functions are functions that can capture anything.
139
141
140
142
A capture annotation `^` binds more strongly than a function arrow. So
141
-
`A -> B^{c}` is read as `A -> (B^{c})`.
143
+
`A -> B^{c}` is read as `A -> (B^{c})` and `A -> B^` is read as `A -> (B^{cap})`.
142
144
143
145
Analogous conventions apply to context function types. `A ?=> B` is an impure context function, with `A ?-> B` as its pure complement.
144
146
@@ -203,15 +205,15 @@ we have
203
205
The set consisting of the root capability `{cap}` covers every other capture set. This is
204
206
a consequence of the fact that, ultimately, every capability is created from `cap`.
205
207
206
-
**Example 2.** Consider again the FileSystem/Logger example from before. `LazyList[Int]` is a proper subtype of `LazyList[Int]^{l}`. So if the `test` method in that example
207
-
was declared with a result type `LazyList[Int]`, we'd get a type error. Here is the error message:
208
+
**Example 2.** Consider again the FileSystem/Logger example from before. `LzyList[Int]` is a proper subtype of `LzyList[Int]^{l}`. So if the `test` method in that example
209
+
was declared with a result type `LzyList[Int]`, we'd get a type error. Here is the error message:
Why does it say `LazyList[Int]^{fs}` and not `LazyList[Int]^{l}`, which is, after all, the type of the returned value `xs`? The reason is that `l` is a local variable in the body of `test`, so it cannot be referred to in a type outside that body. What happens instead is that the type is _widened_ to the smallest supertype that does not mention `l`. Since `l` has capture set `fs`, we have that `{fs}` covers `{l}`, and `{fs}` is acceptable in a result type of `test`, so `{fs}` is the result of that widening.
216
+
Why does it say `LzyList[Int]^{fs}` and not `LzyList[Int]^{l}`, which is, after all, the type of the returned value `xs`? The reason is that `l` is a local variable in the body of `test`, so it cannot be referred to in a type outside that body. What happens instead is that the type is _widened_ to the smallest supertype that does not mention `l`. Since `l` has capture set `fs`, we have that `{fs}` covers `{l}`, and `{fs}` is acceptable in a result type of `test`, so `{fs}` is the result of that widening.
215
217
This widening is called _avoidance_; it is not specific to capture checking but applies to all variable references in Scala types.
216
218
217
219
## Capability Classes
@@ -361,39 +363,37 @@ This principle plays an important part in making capture checking concise and pr
361
363
362
364
## Escape Checking
363
365
364
-
Some capture sets are restricted so that
365
-
they are not allowed to contain the universal capability.
366
366
367
-
Specifically, if a capturing type is an instance of a type variable, that capturing type
368
-
is not allowed to carry the universal capability `cap`. There's a connection to tunnelling here.
369
-
The capture set of a type has to be present in the environment when a type is instantiated from
370
-
a type variable. But `cap` is not itself available as a global entity in the environment. Hence,
371
-
an error should result.
367
+
Capabilities follow the usual scoping discipline, which means that capture sets
368
+
can contain only capabilities that are visible at the point where the set is defined.
372
369
373
-
We can now reconstruct how this principle produced the error in the introductory example, where
370
+
We now reconstruct how this principle produced the error in the introductory example, where
| val later = usingLogFile { f => () => f.write(0) }
381
-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
382
-
|The expression's type () => Unit is not allowed to capture the root capability `cap`.
383
-
|This usually means that a capability persists longer than its allowed lifetime.
378
+
| ^^^^^^^^^^^^^^^^^^^^^^^^^
379
+
| Found: (f: java.io.FileOutputStream^'s1) ->'s2 () ->{f} Unit
380
+
| Required: java.io.FileOutputStream^ => () ->'s3 Unit
381
+
|
382
+
| Note that capability f cannot be included in outer capture set 's3.
384
383
```
385
384
This error message was produced by the following logic:
386
385
387
386
- The `f` parameter has type `FileOutputStream^`, which makes it a capability.
388
387
- Therefore, the type of the expression `() => f.write(0)` is `() ->{f} Unit`.
389
388
- This makes the type of the whole closure passed to `usingLogFile` the dependent function type
390
-
`(f: FileOutputStream^) -> () ->{f} Unit`.
389
+
`(f: FileOutputStream^'s1) ->'s2 () ->{f} Unit`,
390
+
for some as yet uncomputed capture sets `'s1` and `'s2`.
391
391
- The expected type of the closure is a simple, parametric, impure function type `FileOutputStream^ => T`,
392
392
for some instantiation of the type variable `T`.
393
-
-The smallest supertype of the closure's dependent function type that is a parametric function type is
394
-
`FileOutputStream^ => () ->{cap} Unit`
395
-
-Hence, the type variable `T` is instantiated to `() ->{cap} Unit`, or abbreviated `() => Unit`,
396
-
which causes the error.
393
+
-Matching with the found type, `T` must have the shape `() ->'s3 Unit`, for
394
+
some capture set `'s3` defined at the level of value `later`.
395
+
-That capture set cannot include the capability `f` since `f` is locally bound.
396
+
This causes the error.
397
397
398
398
An analogous restriction applies to the type of a mutable variable.
399
399
Another way one could try to undermine capture checking would be to
@@ -406,23 +406,8 @@ usingLogFile { f =>
406
406
}
407
407
loophole()
408
408
```
409
-
But this will not compile either, since mutable variables cannot have universal capture sets.
410
-
411
-
One also needs to prevent returning or assigning a closure with a local capability in an argument of a parametric type. For instance, here is a
412
-
slightly more refined attack:
413
-
```scala
414
-
classCell[+A](x: A)
415
-
valsneaky= usingLogFile { f =>Cell(() => f.write(0)) }
416
-
sneaky.x()
417
-
```
418
-
At the point where the `Cell` is created, the capture set of the argument is `f`, which
419
-
is OK. But at the point of use, it is `cap` (because `f` is no longer in scope), which causes again an error:
420
-
```
421
-
| sneaky.x()
422
-
| ^^^^^^^^
423
-
|The expression's type () => Unit is not allowed to capture the root capability `cap`.
424
-
|This usually means that a capability persists longer than its allowed lifetime.
425
-
```
409
+
But this will not compile either, since the capture set of the mutable variable `loophole` cannot refer to variable `f`, which is not visible
410
+
where `loophole` is defined.
426
411
427
412
Looking at object graphs, we observe a monotonicity property: The capture set of an object `x` covers the capture sets of all objects reachable through `x`. This property is reflected in the type system by the following _monotonicity rule_:
0 commit comments