diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index eda8b6bf567a..c89cc2556eea 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -81,7 +81,7 @@ object CheckCaptures: end Env def definesEnv(sym: Symbol)(using Context): Boolean = - sym.is(Method) || sym.isClass + sym.is(Method) || sym.isClass || sym.is(Lazy) /** Similar normal substParams, but this is an approximating type map that * maps parameters in contravariant capture sets to the empty set. @@ -225,7 +225,7 @@ object CheckCaptures: def needsSepCheck: Boolean /** If a tree is an argument for which needsSepCheck is true, - * the type of the formal paremeter corresponding to the argument. + * the type of the formal parameter corresponding to the argument. */ def formalType: Type @@ -441,7 +441,7 @@ class CheckCaptures extends Recheck, SymTransformer: */ def capturedVars(sym: Symbol)(using Context): CaptureSet = myCapturedVars.getOrElseUpdate(sym, - if sym.isTerm || !sym.owner.isStaticOwner + if sym.isTerm || !sym.owner.isStaticOwner || sym.is(Lazy) then CaptureSet.Var(sym, nestedOK = false) else CaptureSet.empty) @@ -665,8 +665,10 @@ class CheckCaptures extends Recheck, SymTransformer: */ override def recheckIdent(tree: Ident, pt: Type)(using Context): Type = val sym = tree.symbol - if sym.is(Method) then - // If ident refers to a parameterless method, charge its cv to the environment + if sym.is(Method) || sym.is(Lazy) then + // If ident refers to a parameterless method or lazy val, charge its cv to the environment. + // Lazy vals are like parameterless methods: accessing them may trigger initialization + // that uses captured references. includeCallCaptures(sym, sym.info, tree) else if sym.exists && !sym.isStatic then markPathFree(sym.termRef, pt, tree) @@ -744,6 +746,27 @@ class CheckCaptures extends Recheck, SymTransformer: checkUpdate(qualType, tree.srcPos): i"Cannot call update ${tree.symbol} of ${qualType.showRef}" + // Additionally, lazy val initializers should not call update methods on + // non-local exclusive capabilities (capabilities defined outside the lazy val) + if curEnv.owner.is(Lazy) then + qualType.captureSet.elems.foreach: elem => + if elem.isExclusive then + val owner = elem.pathOwner + // Allow update methods on local capabilities (owned by the lazy val or nested within it) + if !owner.isContainedIn(curEnv.owner) && owner != curEnv.owner then + report.error( + em"""Lazy val initializer calls update method on non-local exclusive capability $elem; + |lazy val initializers should only access non-local capabilities in a read-only fashion.""", + tree.srcPos) + + // If selecting a lazy val member, charge the qualifier since accessing + // the lazy val can trigger initialization that uses the qualifier's capabilities + if tree.symbol.is(Lazy) then + qualType match + case tr: (TermRef | ThisType) => + markPathFree(tr, pt, tree) + case _ => + val origSelType = recheckSelection(tree, qualType, name, disambiguate) val selType = mapResultRoots(origSelType, tree.symbol) val selWiden = selType.widen @@ -1103,6 +1126,7 @@ class CheckCaptures extends Recheck, SymTransformer: * - for externally visible definitions: check that their inferred type * does not refine what was known before capture checking. * - Interpolate contravariant capture set variables in result type. + * - for lazy vals: create a nested environment to track captures (similar to methods) */ override def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Type = val savedEnv = curEnv @@ -1125,8 +1149,16 @@ class CheckCaptures extends Recheck, SymTransformer: "" disallowBadRootsIn( tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos) - if runInConstructor then + + // Lazy vals need their own environment to track captures from their RHS, + // similar to how methods work + if sym.is(Lazy) then + val localSet = capturedVars(sym) + if localSet ne CaptureSet.empty then + curEnv = Env(sym, EnvKind.Regular, localSet, curEnv, nestedClosure = NoSymbol) + else if runInConstructor then pushConstructorEnv() + checkInferredResult(super.recheckValDef(tree, sym), tree) finally if !sym.is(Param) then @@ -1140,6 +1172,9 @@ class CheckCaptures extends Recheck, SymTransformer: if runInConstructor && savedEnv.owner.isClass then curEnv = savedEnv markFree(declaredCaptures, tree, addUseInfo = false) + else if sym.is(Lazy) then + // Restore environment after checking lazy val + curEnv = savedEnv if sym.owner.isStaticOwner && !declaredCaptures.elems.isEmpty && sym != defn.captureRoot then def where = diff --git a/docs/_docs/reference/experimental/capture-checking/basics.md b/docs/_docs/reference/experimental/capture-checking/basics.md index 8439810d4528..b2c8ee475ff9 100644 --- a/docs/_docs/reference/experimental/capture-checking/basics.md +++ b/docs/_docs/reference/experimental/capture-checking/basics.md @@ -172,6 +172,63 @@ def f(x: ->{c} Int): Int ``` Here, the actual argument to `f` is allowed to use the `c` capability but no others. +## Lazy Vals + +Lazy vals receive special treatment under capture checking, similar to parameterless methods. A lazy val has two distinct capture sets: + +1. **The initializer's capture set**: What capabilities the initialization code uses +2. **The result's capture set**: What capabilities the lazy val's value captures + +### Initializer Captures + +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: + +```scala +def example(console: Console^) = + lazy val x: () -> String = + console.println("Computing x") // console captured by initializer + () => "Hello, World!" // result doesn't capture console + + val fun: () ->{console} String = () => x() // ok: accessing x uses console + val fun2: () -> String = () => x() // error: x captures console +``` + +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. + +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`. + +### Lazy Val Member Selection + +When accessing a lazy val member through a qualifier, the qualifier is charged to the current capture set, just like calling a parameterless method: + +```scala +trait Container: + lazy val lazyMember: String + +def client(c: Container^): Unit = + val f1: () -> String = () => c.lazyMember // error + val f2: () ->{c} String = () => c.lazyMember // ok +``` + +Accessing `c.lazyMember` can trigger initialization, which may use capabilities from `c`. Therefore, the capture set must include `c`. + +### Equivalence with Methods + +For capture checking purposes, lazy vals behave identically to parameterless methods: + +```scala +trait T: + def methodMember(): String + lazy val lazyMember: String + +def test(t: T^): Unit = + // Both require {t} in the capture set + val m: () ->{t} String = () => t.methodMember() + val l: () ->{t} String = () => t.lazyMember +``` + +This equivalence reflects that both can trigger computation using capabilities from their enclosing object. + ## Subtyping and Subcapturing Capturing influences subtyping. As usual we write `T₁ <: T₂` to express that the type diff --git a/docs/_docs/reference/experimental/capture-checking/mutability.md b/docs/_docs/reference/experimental/capture-checking/mutability.md index 771e939e3467..5613717a5cd1 100644 --- a/docs/_docs/reference/experimental/capture-checking/mutability.md +++ b/docs/_docs/reference/experimental/capture-checking/mutability.md @@ -215,6 +215,67 @@ val b1: Ref^{a.rd} = a val b2: Ref^{cap.rd} = a ``` +## Lazy Vals and Read-Only Restrictions + +Lazy val initializers are subject to read-only restrictions similar to those for normal methods in `Mutable` classes. Specifically, a lazy val initializer cannot call update methods on non-local exclusive capabilities—capabilities defined outside the lazy val's scope. + +### Read-Only Initialization + +When a lazy val is declared, its initializer may use capabilities from the surrounding environment. However, it can only access non-local exclusive capabilities in a read-only fashion: + +```scala +def example(r: Ref^) = + lazy val badInit: () ->{r.rd} Int = + r.set(100) // error: cannot call update method + () => r.get() + + lazy val goodInit: () ->{r.rd} Int = + val i = r.get() // ok: read-only access + () => r.get() + i +``` + +The initializer of `badInit` attempts to call `r.set(100)`, an update method on the non-local exclusive capability `r`. This is rejected because initializers should not perform mutations on external state. + +### Local Capabilities + +The restriction applies only to **non-local** capabilities. A lazy val can freely call update methods on capabilities it creates locally within its initializer: + +```scala +def example = + lazy val localMutation: () => Int = + val local: Ref^ = Ref(10) // created in initializer + local.set(100) // ok: local capability + () => local.get() +``` + +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. + +### Closures vs. Initializer Code + +The read-only restriction applies to code that runs during initialization, not to closures created by the initializer: + +```scala +def example(r: Ref^) = + lazy val closure: () ->{r} Int = + val i = r.get() + () => r.set(i); r.get() // ok: closure runs later, not during init +``` + +Closures (like `() => ...`) run at a later time than the initializer, so their update method calls are permitted. + +### Rationale + +Since lazy val initialization happens unpredictably (on first access), allowing initializers to mutate non-local state could cause subtle bugs. The read-only restriction ensures: + +1. **Predictable initialization**: Accessing a lazy val for the first time doesn't have surprising side effects on external mutable state +2. **Thread safety**: Lazy vals can be safely used in concurrent contexts without worrying about initialization side effects +3. **Referential transparency**: The timing of first access doesn't affect program correctness + +This makes lazy vals behave like normal methods in `Mutable` classes: they can read from their environment but cannot update it unless explicitly marked. +There's currently no `update` modifier for lazy vals, so their initialization is always read-only with respect to non-local capabilities. A future version of capture checking might +support `update lazy val` if there are compelling use cases and there is sufficient +community demand. + ## Update Restrictions 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. diff --git a/library/src/scala/collection/SeqView.scala b/library/src/scala/collection/SeqView.scala index 63ffd17fc109..0d5fb1d9a5e5 100644 --- a/library/src/scala/collection/SeqView.scala +++ b/library/src/scala/collection/SeqView.scala @@ -151,7 +151,7 @@ object SeqView { def apply(i: Int): A = _reversed.apply(i) def length: Int = len - def iterator: Iterator[A] = Iterator.empty ++ _reversed.iterator // very lazy + def iterator: Iterator[A]^{this} = Iterator.empty ++ _reversed.iterator // very lazy override def knownSize: Int = len override def isEmpty: Boolean = len == 0 override def to[C1](factory: Factory[A, C1]): C1 = _reversed.to(factory) diff --git a/tests/neg-custom-args/captures/lazyvals-sep.scala b/tests/neg-custom-args/captures/lazyvals-sep.scala new file mode 100644 index 000000000000..74be6eae4953 --- /dev/null +++ b/tests/neg-custom-args/captures/lazyvals-sep.scala @@ -0,0 +1,113 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.* + +class Ref(x: Int) extends Mutable: + private var value: Int = x + def get(): Int = value + update def set(newValue: Int): Unit = value = newValue + +// For testing types other than functions +class Wrapper(val ref: Ref^) extends Mutable: + def compute(): Int = ref.get() + update def mutate(x: Int): Unit = ref.set(x) + +class WrapperRd(val ref: Ref^{cap.rd}): + def compute(): Int = ref.get() + +@main def run = + val r: Ref^ = Ref(0) + val r2: Ref^ = Ref(42) + + // Test case 1: Read-only access in initializer - should be OK + lazy val lazyVal: () ->{r.rd} Int = + val current = r2.get() + () => r.get() + current + + // Test case 2: Exclusive access in initializer - should error + lazy val lazyVal2: () ->{r.rd} Int = + val current = r2.get() + r.set(current * 100) // error - exclusive access in initializer + () => r.get() + + // Test case 3: Exclusive access in returned closure - should be OK + lazy val lazyVal3: () ->{r} Int = + val current = r2.get() + () => r.set(current); r.get() // exclusive access in closure, not initializer + + // Test case 4: Multiple nested blocks with exclusive access - should error + lazy val lazyVal4: () ->{r.rd} Int = + val x = { + val y = { + r.set(100) // error + r.get() + } + y + 1 + } + () => r.get() + x + + // Test case 5: Multiple nested blocks with only read access - should be OK + lazy val lazyVal5: () ->{r.rd} Int = + val x = { + val y = { + r.get() // only read access in nested blocks + } + y + 1 + } + () => r.get() + x + + // Test case 6: WrapperRd type - exclusive access in initializer - should error + lazy val lazyVal6: WrapperRd^{r} = + r.set(200) // error + WrapperRd(r) + + // Test case 7: WrapperRd type - non-exclusive access in initializer - should be ok + lazy val lazyVal7: WrapperRd^{r} = + r.get() + WrapperRd(r) + + // Test case 8: Wrapper type - exclusive access in initializer - should error + lazy val lazyVal8: Wrapper^{cap, r} = + r.set(200) // error + Wrapper(r) + + // Test case 9: Wrapper type - non-exclusive access in initializer - should be ok + lazy val lazyVal9: Wrapper^{cap, r} = + r.get() + Wrapper(r) + + // Test case 10: Conditional with exclusive access - should error + lazy val lazyVal10: WrapperRd^{r} = + val x = if r.get() > 0 then + r.set(0) // error exclusive access in conditional + 1 + else 2 + WrapperRd(r) + + // Test case 11: Try-catch with exclusive access - should error + lazy val lazyVal11: () ->{r.rd} Int = + val x = try + r.set(42) // error + r.get() + catch + case _: Exception => 0 + () => r.get() + x + + // Test case 12: Local exclusive access - should be OK + lazy val lazyVal12: () => Int = + val r3: Ref^ = Ref(10) + r3.set(100) // ok + val i = r3.get() + () => i + + // Test case 13: Local exclusive access - should be OK + lazy val lazyVal13: () => Int = + val r3: Ref^ = Ref(10) + r3.set(100) // ok + () => r3.get() + + // Test case 14: Local exclusive access - should be OK + lazy val lazyVal14: () => Ref^ = + val r3: Ref^ = Ref(10) + r3.set(100) // ok + () => r3 \ No newline at end of file diff --git a/tests/neg-custom-args/captures/lazyvals.scala b/tests/neg-custom-args/captures/lazyvals.scala new file mode 100644 index 000000000000..5a26b4ce60d5 --- /dev/null +++ b/tests/neg-custom-args/captures/lazyvals.scala @@ -0,0 +1,20 @@ +import language.experimental.captureChecking +import caps.* + +class Console extends SharedCapability: + def println(msg: String): Unit = Predef.println("CONSOLE: " + msg) + +@main def run = + val console: Console^ = Console() + lazy val x: () -> String = { + console.println("Computing x") + () => "Hello, World!" + } + + val fun: () ->{console} String = () => x() // ok + val fun2: () -> String = () => x() // error + val fun3: () ->{x} String = () => x() // error // error + + println("Before accessing x") + println(s"x = ${x()}") + println(s"x again = ${x()}") diff --git a/tests/neg-custom-args/captures/lazyvals2.scala b/tests/neg-custom-args/captures/lazyvals2.scala new file mode 100644 index 000000000000..7733f5a00f01 --- /dev/null +++ b/tests/neg-custom-args/captures/lazyvals2.scala @@ -0,0 +1,19 @@ +import language.experimental.captureChecking +import caps.* + +class Console extends SharedCapability: + def println(msg: String): Unit = Predef.println("CONSOLE: " + msg) + +class IO extends SharedCapability: + def readLine(): String = scala.io.StdIn.readLine() + +@main def run = + val console: Console^ = Console() + val io: IO^ = IO() + lazy val x: () ->{io} String = { + console.println("Computing x") + () => io.readLine() + } + + val fun: () ->{console,io} String = () => x() // ok + val fun2: () ->{io} String = () => x() // error diff --git a/tests/neg-custom-args/captures/lazyvals3.scala b/tests/neg-custom-args/captures/lazyvals3.scala new file mode 100644 index 000000000000..1d1f0b4fe142 --- /dev/null +++ b/tests/neg-custom-args/captures/lazyvals3.scala @@ -0,0 +1,55 @@ +import language.experimental.captureChecking +import caps.* + +class C +type Cap = C^ + +class Console extends SharedCapability: + def println(msg: String): Unit = Predef.println("CONSOLE: " + msg) + +class IO extends SharedCapability: + def readLine(): String = scala.io.StdIn.readLine() + +def test(c: Cap, console: Console^, io: IO^): Unit = + lazy val ev: (Int -> Boolean) = (n: Int) => + lazy val od: (Int -> Boolean) = (n: Int) => + if n == 1 then true else ev(n - 1) + if n == 0 then true else od(n - 1) + + // In a mutually recursive lazy val, the result types accumulate the captures of both the initializers and results themselves. + // So, this is not ok: + lazy val ev1: (Int ->{io,console} Boolean) = + println(c) + (n: Int) => + lazy val od1: (Int ->{ev1,console} Boolean) = (n: Int) => // error + if n == 1 then + console.println("CONSOLE: 1") + true + else + ev1(n - 1) + if n == 0 then + io.readLine() // just to capture io + true + else + od1(n - 1) + + // But this is ok: + lazy val ev2: (Int ->{c,io,console} Boolean) = + println(c) + (n: Int) => + lazy val od2: (Int ->{c,io,console} Boolean) = (n: Int) => + if n == 1 then + console.println("CONSOLE: 1") + true + else + ev2(n - 1) + if n == 0 then + io.readLine() // just to capture io + true + else + od2(n - 1) + + val even: Int -> Boolean = (n: Int) => ev(n) // ok + val even2: Int ->{io,console,c} Boolean = (n: Int) => ev1(n) // ok + + () \ No newline at end of file diff --git a/tests/neg-custom-args/captures/lazyvals4.scala b/tests/neg-custom-args/captures/lazyvals4.scala new file mode 100644 index 000000000000..a062dee25de1 --- /dev/null +++ b/tests/neg-custom-args/captures/lazyvals4.scala @@ -0,0 +1,29 @@ +import language.experimental.captureChecking +import caps.* + +class Console extends SharedCapability: + def println(msg: String): Unit = Predef.println("CONSOLE: " + msg) + +class IO extends SharedCapability: + def readLine(): String = scala.io.StdIn.readLine() + +class Clazz(val console: Console^): + lazy val memberLazy: () -> String = { + console.println("Computing memberLazy") + () => "Member Lazy Value" + } + +trait Trait: + lazy val memberLazy: () -> String + def memberMethod(): String + +def client(t: Trait^, c: Clazz^): Unit = + val v0: () -> () -> String = () => t.memberLazy // error + val v0_1: () ->{t} () -> String = () => t.memberLazy // ok + val v1: () -> String = () => t.memberLazy() // error + val v2: (() -> String)^{t} = () => t.memberLazy() // ok + val v3: (() -> String)^{c.console} = () => c.memberLazy() // error (but should this be allowed?) + val v4: () -> String = () => t.memberMethod() // error + val v5: (() -> String)^{t} = () => t.memberMethod() // ok + + () \ No newline at end of file diff --git a/tests/neg-custom-args/captures/lazyvals5.scala b/tests/neg-custom-args/captures/lazyvals5.scala new file mode 100644 index 000000000000..50e32aed58ec --- /dev/null +++ b/tests/neg-custom-args/captures/lazyvals5.scala @@ -0,0 +1,63 @@ +import language.experimental.captureChecking +import caps.* + +class Console extends SharedCapability: + def println(msg: String): Unit = Predef.println("CONSOLE: " + msg) + +class IO extends SharedCapability: + def readLine(): String = scala.io.StdIn.readLine() + +class Clazz(val console: Console^): + val io: IO^ = IO() + lazy val memberLazy: () ->{io} String = { + console.println("Computing memberLazy") + () => "Member Lazy Value" + io.readLine() + } + +def client(c: Clazz^): Unit = + val io: IO^ = IO() + trait Trait: + lazy val memberLazy: () ->{io} String + def memberMethod(): String + + val t: Trait^ = ??? + + lazy val funky = t.memberLazy() + c.memberLazy() + + lazy val anotherFunky = + c.console.println("Computing anotherFunky") + t.memberLazy + + val v0: () -> () ->{io} String = () => t.memberLazy // error + val v0_1: () ->{t} () ->{io} String = () => t.memberLazy // ok + val v1: () -> String = () => t.memberLazy() // error + val v2: (() -> String)^{t} = () => t.memberLazy() // ok + val v3: (() -> String)^{c.console} = () => c.memberLazy() // error (but should this be allowed?) + val v4: () -> String = () => t.memberMethod() // error + val v5: (() -> String)^{t} = () => t.memberMethod() // ok + + val v6: () ->{c} String = () => funky // error + val v6_1: () ->{t} String = () => funky // error + val v7: () ->{c, t} String = () => funky // ok + + val v8: () ->{t, c.console} String = () => anotherFunky() // ok + + class Clazz2(val console: Console^): + val io: IO^ = IO() + final lazy val memberLazy: () ->{io} String = { + console.println("Computing memberLazy") + () => "Member Lazy Value" + io.readLine() + } + + trait Trait2: + final lazy val memberLazy : () ->{io} String = () => io.readLine() + + val c2: Clazz2^ = ??? + val t2: Trait2^ = ??? + + lazy val funky2 = t2.memberLazy() + c2.memberLazy() + + val v9: () ->{c2.memberLazy, t2.memberLazy} String = () => funky2 // error (but should this be allowed?) + val v10: () ->{t2, c2} String = () => funky2 // ok + + () \ No newline at end of file