Skip to content

Commit 13372c9

Browse files
authored
Capture Checking of Lazy Vals (#24261)
## Add capture checking support for lazy vals Fixes #21601 Extends capture checking to handle lazy vals, treating them like parameterless methods for capture tracking. ## Key Changes 1. Lazy val environments. Lazy vals now create their own environment to track initializer captures, separate from the result type's capture set. 2. Member selection. When accessing a lazy val member (e.g., `t.lazyMember`), the qualifier `t` is charged to the capture set, reflecting that initialization may use the qualifier's capabilities. 3. Read-only initialization. For lazy val fields of `Mutable` classes, their initializers cannot call update methods on non-local exclusive capabilities (just like non-update methods). 4. Documentation in the language reference. 5. Fix errors in the standard library revealed by proper lazy vals support.
1 parent 628ae98 commit 13372c9

File tree

17 files changed

+654
-22
lines changed

17 files changed

+654
-22
lines changed

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

Lines changed: 23 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ object CheckCaptures:
8181
end Env
8282

8383
def definesEnv(sym: Symbol)(using Context): Boolean =
84-
sym.is(Method) || sym.isClass
84+
sym.isOneOf(MethodOrLazy) || sym.isClass
8585

8686
/** Similar normal substParams, but this is an approximating type map that
8787
* maps parameters in contravariant capture sets to the empty set.
@@ -225,7 +225,7 @@ object CheckCaptures:
225225
def needsSepCheck: Boolean
226226

227227
/** If a tree is an argument for which needsSepCheck is true,
228-
* the type of the formal paremeter corresponding to the argument.
228+
* the type of the formal parameter corresponding to the argument.
229229
*/
230230
def formalType: Type
231231

@@ -441,7 +441,7 @@ class CheckCaptures extends Recheck, SymTransformer:
441441
*/
442442
def capturedVars(sym: Symbol)(using Context): CaptureSet =
443443
myCapturedVars.getOrElseUpdate(sym,
444-
if sym.isTerm || !sym.owner.isStaticOwner
444+
if sym.isTerm || !sym.owner.isStaticOwner || sym.is(Lazy)
445445
then CaptureSet.Var(sym, nestedOK = false)
446446
else CaptureSet.empty)
447447

@@ -578,7 +578,7 @@ class CheckCaptures extends Recheck, SymTransformer:
578578
if !isOfNestedMethod(env) then
579579
val nextEnv = nextEnvToCharge(env)
580580
if nextEnv != null && !nextEnv.owner.isStaticOwner then
581-
if env.owner.isReadOnlyMethod && nextEnv.owner != env.owner then
581+
if env.owner.isReadOnlyMethodOrLazyVal && nextEnv.owner != env.owner then
582582
checkReadOnlyMethod(included, env)
583583
recur(included, nextEnv, env)
584584
// Under deferredReaches, don't propagate out of methods inside terms.
@@ -665,8 +665,10 @@ class CheckCaptures extends Recheck, SymTransformer:
665665
*/
666666
override def recheckIdent(tree: Ident, pt: Type)(using Context): Type =
667667
val sym = tree.symbol
668-
if sym.is(Method) then
669-
// If ident refers to a parameterless method, charge its cv to the environment
668+
if sym.isOneOf(MethodOrLazy) then
669+
// If ident refers to a parameterless method or lazy val, charge its cv to the environment.
670+
// Lazy vals are like parameterless methods: accessing them may trigger initialization
671+
// that uses captured references.
670672
includeCallCaptures(sym, sym.info, tree)
671673
else if sym.exists && !sym.isStatic then
672674
markPathFree(sym.termRef, pt, tree)
@@ -688,7 +690,7 @@ class CheckCaptures extends Recheck, SymTransformer:
688690
case pt: PathSelectionProto if ref.isTracked =>
689691
// if `ref` is not tracked then the selection could not give anything new
690692
// class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters.
691-
if pt.select.symbol.isReadOnlyMethod then
693+
if pt.select.symbol.isReadOnlyMethodOrLazyVal then
692694
markFree(ref.readOnly, tree)
693695
else
694696
val sel = ref.select(pt.select.symbol).asInstanceOf[TermRef]
@@ -708,8 +710,8 @@ class CheckCaptures extends Recheck, SymTransformer:
708710
*/
709711
override def selectionProto(tree: Select, pt: Type)(using Context): Type =
710712
val sym = tree.symbol
711-
if !sym.isOneOf(UnstableValueFlags) && !sym.isStatic
712-
|| sym.isReadOnlyMethod
713+
if !sym.isOneOf(MethodOrLazyOrMutable) && !sym.isStatic
714+
|| sym.isReadOnlyMethodOrLazyVal
713715
then PathSelectionProto(tree, pt)
714716
else super.selectionProto(tree, pt)
715717

@@ -1103,6 +1105,7 @@ class CheckCaptures extends Recheck, SymTransformer:
11031105
* - for externally visible definitions: check that their inferred type
11041106
* does not refine what was known before capture checking.
11051107
* - Interpolate contravariant capture set variables in result type.
1108+
* - for lazy vals: create a nested environment to track captures (similar to methods)
11061109
*/
11071110
override def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Type =
11081111
val savedEnv = curEnv
@@ -1125,8 +1128,16 @@ class CheckCaptures extends Recheck, SymTransformer:
11251128
""
11261129
disallowBadRootsIn(
11271130
tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos)
1128-
if runInConstructor then
1131+
1132+
// Lazy vals need their own environment to track captures from their RHS,
1133+
// similar to how methods work
1134+
if sym.is(Lazy) then
1135+
val localSet = capturedVars(sym)
1136+
if localSet ne CaptureSet.empty then
1137+
curEnv = Env(sym, EnvKind.Regular, localSet, curEnv, nestedClosure = NoSymbol)
1138+
else if runInConstructor then
11291139
pushConstructorEnv()
1140+
11301141
checkInferredResult(super.recheckValDef(tree, sym), tree)
11311142
finally
11321143
if !sym.is(Param) then
@@ -1137,8 +1148,9 @@ class CheckCaptures extends Recheck, SymTransformer:
11371148
interpolateIfInferred(tree.tpt, sym)
11381149

11391150
def declaredCaptures = tree.tpt.nuType.captureSet
1151+
curEnv = savedEnv
1152+
11401153
if runInConstructor && savedEnv.owner.isClass then
1141-
curEnv = savedEnv
11421154
markFree(declaredCaptures, tree, addUseInfo = false)
11431155

11441156
if sym.owner.isStaticOwner && !declaredCaptures.elems.isEmpty && sym != defn.captureRoot then

compiler/src/dotty/tools/dotc/cc/Mutability.scala

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -53,21 +53,21 @@ object Mutability:
5353
sym.isAllOf(Mutable | Method)
5454
&& (!sym.isSetter || sym.field.is(Transparent))
5555

56-
/** A read-only methid is a real method (not an accessor) in a type extending
57-
* Mutable that is not an update method.
56+
/** A read-only method is a real method (not an accessor) in a type extending
57+
* Mutable that is not an update method. Included are also lazy vals in such types.
5858
*/
59-
def isReadOnlyMethod(using Context): Boolean =
60-
sym.is(Method, butNot = Mutable | Accessor) && sym.owner.derivesFrom(defn.Caps_Mutable)
59+
def isReadOnlyMethodOrLazyVal(using Context): Boolean =
60+
sym.isOneOf(MethodOrLazy, butNot = Mutable | Accessor)
61+
&& sym.owner.derivesFrom(defn.Caps_Mutable)
6162

6263
private def inExclusivePartOf(cls: Symbol)(using Context): Exclusivity =
6364
import Exclusivity.*
64-
val encl = sym.enclosingMethodOrClass.skipConstructor
6565
if sym == cls then OK // we are directly in `cls` or in one of its constructors
66-
else if encl.owner == cls then
67-
if encl.isUpdateMethod then OK
68-
else NotInUpdateMethod(encl, cls)
69-
else if encl.isStatic then OutsideClass(cls)
70-
else encl.owner.inExclusivePartOf(cls)
66+
else if sym.owner == cls then
67+
if sym.isUpdateMethod || sym.isConstructor then OK
68+
else NotInUpdateMethod(sym, cls)
69+
else if sym.isStatic then OutsideClass(cls)
70+
else sym.owner.inExclusivePartOf(cls)
7171

7272
extension (tp: Type)
7373
/** Is this a type extending `Mutable` that has non-private update methods

docs/_docs/reference/experimental/capture-checking/basics.md

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,63 @@ def f(x: ->{c} Int): Int
172172
```
173173
Here, the actual argument to `f` is allowed to use the `c` capability but no others.
174174

175+
## Lazy Vals
176+
177+
Lazy vals receive special treatment under capture checking, similar to parameterless methods. A lazy val has two distinct capture sets:
178+
179+
1. **The initializer's capture set**: What capabilities the initialization code uses
180+
2. **The result's capture set**: What capabilities the lazy val's value captures
181+
182+
### Initializer Captures
183+
184+
When a lazy val is declared, its initializer is checked in its own environment (like a method body). The initializer can capture capabilities, and these are tracked separately:
185+
186+
```scala
187+
def example(console: Console^) =
188+
lazy val x: () -> String =
189+
console.println("Computing x") // console captured by initializer
190+
() => "Hello, World!" // result doesn't capture console
191+
192+
val fun: () ->{console} String = () => x() // ok: accessing x uses console
193+
val fun2: () -> String = () => x() // error: x captures console
194+
```
195+
196+
Here, the initializer of `x` uses `console` (to print a message), so accessing `x` for the first time will use the `console` capability. However, the **result** of `x` is a pure function `() -> String` that doesn't capture any capabilities.
197+
198+
The type system tracks that accessing `x` requires the `console` capability, even though the resulting value doesn't. This is reflected in the function types: `fun` must declare `{console}` in its capture set because it accesses `x`.
199+
200+
### Lazy Val Member Selection
201+
202+
When accessing a lazy val member through a qualifier, the qualifier is charged to the current capture set, just like calling a parameterless method:
203+
204+
```scala
205+
trait Container:
206+
lazy val lazyMember: String
207+
208+
def client(c: Container^): Unit =
209+
val f1: () -> String = () => c.lazyMember // error
210+
val f2: () ->{c} String = () => c.lazyMember // ok
211+
```
212+
213+
Accessing `c.lazyMember` can trigger initialization, which may use capabilities from `c`. Therefore, the capture set must include `c`.
214+
215+
### Equivalence with Methods
216+
217+
For capture checking purposes, lazy vals behave identically to parameterless methods:
218+
219+
```scala
220+
trait T:
221+
def methodMember: String
222+
lazy val lazyMember: String
223+
224+
def test(t: T^): Unit =
225+
// Both require {t} in the capture set
226+
val m: () ->{t} String = () => t.methodMember
227+
val l: () ->{t} String = () => t.lazyMember
228+
```
229+
230+
This equivalence reflects that both can trigger computation using capabilities from their enclosing object.
231+
175232
## Subtyping and Subcapturing
176233

177234
Capturing influences subtyping. As usual we write `T₁ <: T₂` to express that the type

docs/_docs/reference/experimental/capture-checking/mutability.md

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -215,6 +215,50 @@ val b1: Ref^{a.rd} = a
215215
val b2: Ref^{cap.rd} = a
216216
```
217217

218+
## Lazy Vals and Read-Only Restrictions
219+
220+
Lazy val initializers in `Mutable` classes are subject to read-only restrictions similar to those for normal methods. Specifically, a lazy val initializer in a `Mutable` class cannot call update methods or refer to non-local exclusive capabilities, i.e., capabilities defined outside the lazy val's scope.
221+
222+
For example, when a lazy val is declared in a local method's scope, its initializer may freely use capabilities from the surrounding environment:
223+
```scala
224+
def example(r: Ref[Int]^) =
225+
lazy val goodInit: () ->{r.rd} Int =
226+
val i = r.get() // ok: read-only access
227+
r.set(100 * i) // ok: can call update method
228+
() => r.get() + i
229+
```
230+
However, within a `Mutable` class, a lazy val declaration has only read access to non-local exclusive capabilities:
231+
```scala
232+
class Wrapper(val r: Ref[Int]^) extends Mutable:
233+
lazy val badInit: () ->{r} Int =
234+
r.set(100) // error: call to update method
235+
() => r.set(r.get() * 2); r.get() // error: call to update method
236+
237+
lazy val goodInit: () ->{r.rd} Int =
238+
val i = r.get() // ok
239+
() => r.get() * i // ok
240+
```
241+
The initializer of `badInit` attempts to call `r.set(100)`, an update method on the non-local exclusive capability `r`.
242+
This is rejected because initializers should not perform mutations on external state.
243+
244+
### Local Capabilities
245+
246+
The restriction applies only to **non-local** capabilities. A lazy val can freely call update methods on capabilities it creates locally within its initializer:
247+
248+
```scala
249+
class Example:
250+
lazy val localMutation: () => Int =
251+
val local: Ref[Int]^ = Ref(10) // created in initializer
252+
local.set(100) // ok: local capability
253+
() => local.get()
254+
```
255+
256+
Here, `local` is created within the lazy val's initializer, so it counts as a local capability. The initializer can call update methods on it.
257+
258+
This makes lazy vals behave like normal methods in `Mutable` classes: they can read from their environment but cannot update it unless explicitly marked.
259+
Unlike for methods, there's currently no `update` modifier for lazy vals in `Mutable` classes, so their initialization is always read-only with respect to non-local capabilities. A future version of capture checking might
260+
support `update lazy val` if there are compelling use cases and there is sufficient community demand.
261+
218262
## Update Restrictions
219263

220264
If a capability `r` is a read-only access, then one cannot use `r` to call an update method of `r` or to assign to a field of `r`. E.g. `r.set(22)` and `r.current = 22` are both disallowed.

library/src/scala/collection/SeqView.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -151,7 +151,7 @@ object SeqView {
151151

152152
def apply(i: Int): A = _reversed.apply(i)
153153
def length: Int = len
154-
def iterator: Iterator[A] = Iterator.empty ++ _reversed.iterator // very lazy
154+
def iterator: Iterator[A]^{this} = Iterator.empty ++ _reversed.iterator // very lazy
155155
override def knownSize: Int = len
156156
override def isEmpty: Boolean = len == 0
157157
override def to[C1](factory: Factory[A, C1]): C1 = _reversed.to(factory)
Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:30:6 -------------------------------------------------------
2+
30 | r.set(current * 100) // error - exclusive access in initializer
3+
| ^^^^^
4+
| Cannot call update method set of TestClass.this.r
5+
| since the access is in lazy value lazyVal2, which is not an update method.
6+
-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:36:12 ------------------------------------------------------
7+
36 | () => r.set(current); r.get() // error, even though exclusive access is in closure, not initializer
8+
| ^^^^^
9+
| Cannot call update method set of TestClass.this.r
10+
| since the access is in lazy value lazyVal3, which is not an update method.
11+
-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:42:10 ------------------------------------------------------
12+
42 | r.set(100) // error
13+
| ^^^^^
14+
| Cannot call update method set of TestClass.this.r
15+
| since the access is in lazy value lazyVal4, which is not an update method.
16+
-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:61:6 -------------------------------------------------------
17+
61 | r.set(200) // error
18+
| ^^^^^
19+
| Cannot call update method set of TestClass.this.r
20+
| since the access is in lazy value lazyVal6, which is not an update method.
21+
-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:71:6 -------------------------------------------------------
22+
71 | r.set(200) // error
23+
| ^^^^^
24+
| Cannot call update method set of TestClass.this.r
25+
| since the access is in lazy value lazyVal8, which is not an update method.
26+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyvals-sep.scala:72:12 ---------------------------------
27+
72 | Wrapper(r) // error
28+
| ^
29+
|Found: Ref^{TestClass.this.r.rd}
30+
|Required: Ref^
31+
|
32+
|Note that capability TestClass.this.r.rd is not included in capture set {}.
33+
|
34+
|Note that {cap} is an exclusive capture set of the mutable type Ref^,
35+
|it cannot subsume a read-only capture set of the mutable type Ref^{TestClass.this.r.rd}.
36+
|
37+
|where: ^ and cap refer to a fresh root capability classified as Mutable created in lazy value lazyVal8 when checking argument to parameter ref of constructor Wrapper
38+
|
39+
| longer explanation available when compiling with `-explain`
40+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyvals-sep.scala:77:12 ---------------------------------
41+
77 | Wrapper(r) // error
42+
| ^
43+
|Found: Ref^{TestClass.this.r.rd}
44+
|Required: Ref^
45+
|
46+
|Note that capability TestClass.this.r.rd is not included in capture set {}.
47+
|
48+
|Note that {cap} is an exclusive capture set of the mutable type Ref^,
49+
|it cannot subsume a read-only capture set of the mutable type Ref^{TestClass.this.r.rd}.
50+
|
51+
|where: ^ and cap refer to a fresh root capability classified as Mutable created in lazy value lazyVal9 when checking argument to parameter ref of constructor Wrapper
52+
|
53+
| longer explanation available when compiling with `-explain`
54+
-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:82:8 -------------------------------------------------------
55+
82 | r.set(0) // error exclusive access in conditional
56+
| ^^^^^
57+
| Cannot call update method set of TestClass.this.r
58+
| since the access is in lazy value lazyVal10, which is not an update method.
59+
-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:90:8 -------------------------------------------------------
60+
90 | r.set(42) // error
61+
| ^^^^^
62+
| Cannot call update method set of TestClass.this.r
63+
| since the access is in lazy value lazyVal11, which is not an update method.

0 commit comments

Comments
 (0)