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
1. Have @use annotation on type parameters and value parameters of regular methods
5
+
(not anonymous functions).
6
+
2. In markFree, keep track whether a capture set variable or reach capability
7
+
is used directly in the method where it is defined, or in a nested context
8
+
(either unbound nested closure or unbound anonymous class).
9
+
3. Disallow charging a reach capability `xs*` to the environment of the method where
10
+
`xs` is a parameter unless `xs` is declared `@use`.
11
+
4. Analogously, disallow charging a capture set variable `C^` to the environment of the method where `C^` is a parameter unless `C^` is declared `@use`.
12
+
5. When passing an argument to a `@use`d term parameter, charge the `dcs` of the argument type to the environments via markFree.
13
+
6. When instantiating a `@use`d type parameter, charge the capture set of the argument
14
+
to the environments via markFree.
15
+
16
+
It follows that we cannot refer to methods with @use term parameters as values. Indeed,
17
+
their eta expansion would produce an anonymous function that includes a reach capability of
Note that `xs` does not carry a `@use` since this is disallowed by (1) for anonymous functions. By (5), we charge the deep capture set of `xs`, which is `xs*` to the environment. By (3), this is actually disallowed.
30
+
31
+
Now, if we express this with explicit capture set parameters we get:
Then `runOpsPoly` expands to `runOpsPoly[cs]` for some inferred capture set `cs`. And this expands to:
36
+
```scala
37
+
(xs: List[() ->{cs} Unit]) => runOpsPoly[cs](xs)
38
+
```
39
+
Since `cs` is passed to the `@use` parameter of `runOpsPoly` it is charged
40
+
to the environment of the function body, so the type of the previous expression is
41
+
```scala
42
+
List[() ->{cs} Unit]) ->{cs} Unit
43
+
```
44
+
45
+
We can also use explicit capture set parameters to eta expand the first `runOps` manually:
46
+
47
+
```scala
48
+
[C^] => (xs: List[() ->{C^} Unit]) => runOps(xs)
49
+
: [C^] ->List[() ->{C^} Unit] ->[C^] Unit
50
+
```
51
+
Except that this currently runs afoul of the implementation restriction that polymorphic functions cannot wrap capturing functions. But that's a restriction we need to lift anyway.
52
+
53
+
## `@use` inference
54
+
55
+
-`@use` is implied for a term parameter `x` of a method if `x`'s type contains a boxed cap and `x` or `x*` is not referred to in the result type of the method.
56
+
57
+
-`@use` is implied for a capture set parameter `C` of a method if `C` is not referred to in the result type of the method.
58
+
59
+
If `@use` is implied, one can override to no use by giving an explicit use annotation
0 commit comments