|
| 1 | +--- |
| 2 | +layout: doc-page |
| 3 | +title: "Capture Checking of Classes" |
| 4 | +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/cc-classes.html |
| 5 | +--- |
| 6 | + |
| 7 | +## Capture Checking of Classes |
| 8 | + |
| 9 | +The principles for capture checking closures also apply to classes. For instance, consider: |
| 10 | +```scala |
| 11 | +class Logger(using fs: FileSystem): |
| 12 | + def log(s: String): Unit = ... summon[FileSystem] ... |
| 13 | + |
| 14 | +def test(xfs: FileSystem): Logger^{xfs} = |
| 15 | + Logger(xfs) |
| 16 | +``` |
| 17 | +Here, class `Logger` retains the capability `fs` as a (private) field. Hence, the result |
| 18 | +of `test` is of type `Logger^{xfs}` |
| 19 | + |
| 20 | +Sometimes, a tracked capability is meant to be used only in the constructor of a class, but |
| 21 | +is not intended to be retained as a field. This fact can be communicated to the capture |
| 22 | +checker by declaring the parameter as `@constructorOnly`. Example: |
| 23 | +```scala |
| 24 | +import annotation.constructorOnly |
| 25 | + |
| 26 | +class NullLogger(using @constructorOnly fs: FileSystem): |
| 27 | + ... |
| 28 | +def test2(using fs: FileSystem): NullLogger = NullLogger() // OK |
| 29 | +``` |
| 30 | + |
| 31 | +The captured references of a class include _local capabilities_ and _argument capabilities_. Local capabilities are capabilities defined outside the class and referenced from its body. Argument capabilities are passed as parameters to the primary constructor of the class. Local capabilities are inherited: |
| 32 | +the local capabilities of a superclass are also local capabilities of its subclasses. Example: |
| 33 | + |
| 34 | +```scala |
| 35 | +class Cap extends caps.SharedCapability |
| 36 | + |
| 37 | +def test(a: Cap, b: Cap, c: Cap) = |
| 38 | + class Super(y: Cap): |
| 39 | + def f = a |
| 40 | + class Sub(x: Cap) extends Super(x) |
| 41 | + def g = b |
| 42 | + Sub(c) |
| 43 | +``` |
| 44 | +Here class `Super` has local capability `a`, which gets inherited by class |
| 45 | +`Sub` and is combined with `Sub`'s own local capability `b`. Class `Sub` also has an argument capability corresponding to its parameter `x`. This capability gets instantiated to `c` in the final constructor call `Sub(c)`. Hence, |
| 46 | +the capture set of that call is `{a, b, c}`. |
| 47 | + |
| 48 | +The capture set of the type of `this` of a class is inferred by the capture checker, unless the type is explicitly declared with a self type annotation like this one: |
| 49 | +```scala |
| 50 | +class C: |
| 51 | + self: D^{a, b} => ... |
| 52 | +``` |
| 53 | +The inference observes the following constraints: |
| 54 | + |
| 55 | + - The type of `this` of a class `C` includes all captured references of `C`. |
| 56 | + - The type of `this` of a class `C` is a subtype of the type of `this` |
| 57 | + of each parent class of `C`. |
| 58 | + - The type of `this` must observe all constraints where `this` is used. |
| 59 | + |
| 60 | +For instance, in |
| 61 | +```scala |
| 62 | +class Cap extends caps.SharedCapability |
| 63 | +def test(c: Cap) = |
| 64 | + class A: |
| 65 | + val x: A = this |
| 66 | + def f = println(c) // error |
| 67 | +``` |
| 68 | +we know that the type of `this` must be pure, since `this` is the right hand side of a `val` with type `A`. However, in the last line we find that the capture set of the class, and with it the capture set of `this`, would include `c`. This leads to a contradiction, and hence to a checking error: |
| 69 | +``` |
| 70 | + | def f = println(c) // error |
| 71 | + | ^ |
| 72 | + | reference (c : Cap) is not included in the allowed capture set {} |
| 73 | + | of the enclosing class A |
| 74 | +``` |
| 75 | + |
| 76 | +## Capture Tunnelling |
| 77 | + |
| 78 | +Consider the following simple definition of a `Pair` class: |
| 79 | +```scala |
| 80 | +class Pair[+A, +B](x: A, y: B): |
| 81 | + def fst: A = x |
| 82 | + def snd: B = y |
| 83 | +``` |
| 84 | +What happens if `Pair` is instantiated like this (assuming `ct` and `fs` are two capabilities in scope)? |
| 85 | +```scala |
| 86 | +def x: Int ->{ct} String |
| 87 | +def y: Logger^{fs} |
| 88 | +def p = Pair(x, y) |
| 89 | +``` |
| 90 | +The last line will be typed as follows: |
| 91 | +```scala |
| 92 | +def p: Pair[Int ->{ct} String, Logger^{fs}] = Pair(x, y) |
| 93 | +``` |
| 94 | +This might seem surprising. The `Pair(x, y)` value does capture capabilities `ct` and `fs`. Why don't they show up in its type at the outside? |
| 95 | + |
| 96 | +The answer is capture tunnelling. Once a type variable is instantiated to a capturing type, the |
| 97 | +capture is not propagated beyond this point. On the other hand, if the type variable is instantiated |
| 98 | +again on access, the capture information "pops out" again. For instance, even though `p` is technically pure because its capture set is empty, writing `p.fst` would record a reference to the captured capability `ct`. So if this access was put in a closure, the capability would again form part of the outer capture set. E.g. |
| 99 | +```scala |
| 100 | +() => p.fst : () -> Int ->{ct} String |
| 101 | +``` |
| 102 | +In other words, references to capabilities "tunnel through" in generic instantiations from creation to access; they do not affect the capture set of the enclosing generic data constructor applications. |
| 103 | +This principle plays an important part in making capture checking concise and practical. |
| 104 | + |
| 105 | + |
| 106 | +## A Larger Example |
| 107 | + |
| 108 | +As a larger example, we present an implementation of lazy lists and some use cases. For simplicity, |
| 109 | +our lists are lazy only in their tail part. This corresponds to what the Scala-2 type `Stream` did, whereas Scala 3's `LazyList` type computes strictly less since it is also lazy in the first argument. |
| 110 | + |
| 111 | +Here is the base trait `LzyList` for our version of lazy lists: |
| 112 | +```scala |
| 113 | +trait LzyList[+A]: |
| 114 | + def isEmpty: Boolean |
| 115 | + def head: A |
| 116 | + def tail: LzyList[A]^{this} |
| 117 | +``` |
| 118 | +Note that `tail` carries a capture annotation. It says that the tail of a lazy list can |
| 119 | +potentially capture the same references as the lazy list as a whole. |
| 120 | + |
| 121 | +The empty case of a `LzyList` is written as usual: |
| 122 | +```scala |
| 123 | +object LzyNil extends LzyList[Nothing]: |
| 124 | + def isEmpty = true |
| 125 | + def head = ??? |
| 126 | + def tail = ??? |
| 127 | +``` |
| 128 | +Here is a formulation of the class for lazy cons nodes: |
| 129 | +```scala |
| 130 | +import scala.compiletime.uninitialized |
| 131 | + |
| 132 | +final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]: |
| 133 | + private var forced = false |
| 134 | + private var cache: LzyList[A]^{this} = uninitialized |
| 135 | + private def force = |
| 136 | + if !forced then { cache = tl(); forced = true } |
| 137 | + cache |
| 138 | + |
| 139 | + def isEmpty = false |
| 140 | + def head = hd |
| 141 | + def tail: LzyList[A]^{this} = force |
| 142 | +end LzyCons |
| 143 | +``` |
| 144 | +The `LzyCons` class takes two parameters: A head `hd` and a tail `tl`, which is a function |
| 145 | +returning a `LzyList`. Both the function and its result can capture arbitrary capabilities. |
| 146 | +The result of applying the function is memoized after the first dereference of `tail` in |
| 147 | +the private mutable field `cache`. Note that the typing of the assignment `cache = tl()` relies on the monotonicity rule for `{this}` capture sets. |
| 148 | + |
| 149 | +Here is an extension method to define an infix cons operator `#:` for lazy lists. It is analogous |
| 150 | +to `::` but instead of a strict list it produces a lazy list without evaluating its right operand. |
| 151 | +```scala |
| 152 | +extension [A](x: A) |
| 153 | + def #:(xs1: => LzyList[A]^): LzyList[A]^{xs1} = |
| 154 | + LzyCons(x, () => xs1) |
| 155 | +``` |
| 156 | +Note that `#:` takes an impure call-by-name parameter `xs1` as its right argument. The result |
| 157 | +of `#:` is a lazy list that captures that argument. |
| 158 | + |
| 159 | +As an example usage of `#:`, here is a method `tabulate` that creates a lazy list |
| 160 | +of given length with a generator function `gen`. The generator function is allowed |
| 161 | +to have side effects. |
| 162 | +```scala |
| 163 | +def tabulate[A](n: Int)(gen: Int => A): LzyList[A]^{gen} = |
| 164 | + def recur(i: Int): LzyList[A]^{gen} = |
| 165 | + if i == n then LzyNil |
| 166 | + else gen(i) #: recur(i + 1) |
| 167 | + recur(0) |
| 168 | +``` |
| 169 | +Here is a use of `tabulate`: |
| 170 | +```scala |
| 171 | +class LimitExceeded extends Exception |
| 172 | +def squares(n: Int)(using ct: CanThrow[LimitExceeded]) = |
| 173 | + tabulate(10): i => |
| 174 | + if i > 9 then throw LimitExceeded() |
| 175 | + i * i |
| 176 | +``` |
| 177 | +The inferred result type of `squares` is `LzyList[Int]^{ct}`, i.e it is a lazy list of |
| 178 | +`Int`s that can throw the `LimitExceeded` exception when it is elaborated by calling `tail` |
| 179 | +one or more times. |
| 180 | + |
| 181 | +Here are some further extension methods for mapping, filtering, and concatenating lazy lists: |
| 182 | +```scala |
| 183 | +extension [A](xs: LzyList[A]^) |
| 184 | + def map[B](f: A => B): LzyList[B]^{xs, f} = |
| 185 | + if xs.isEmpty then LzyNil |
| 186 | + else f(xs.head) #: xs.tail.map(f) |
| 187 | + |
| 188 | + def filter(p: A => Boolean): LzyList[A]^{xs, p} = |
| 189 | + if xs.isEmpty then LzyNil |
| 190 | + else if p(xs.head) then xs.head #: xs.tail.filter(p) |
| 191 | + else xs.tail.filter(p) |
| 192 | + |
| 193 | + def concat(ys: LzyList[A]^): LzyList[A]^{xs, ys} = |
| 194 | + if xs.isEmpty then ys |
| 195 | + else xs.head #: xs.tail.concat(ys) |
| 196 | + |
| 197 | + def drop(n: Int): LzyList[A]^{xs} = |
| 198 | + if n == 0 then xs else xs.tail.drop(n - 1) |
| 199 | +``` |
| 200 | +Their capture annotations are all as one would expect: |
| 201 | + |
| 202 | + - Mapping a lazy list produces a lazy list that captures the original list as well |
| 203 | + as the (possibly impure) mapping function. |
| 204 | + - Filtering a lazy list produces a lazy list that captures the original list as well |
| 205 | + as the (possibly impure) filtering predicate. |
| 206 | + - Concatenating two lazy lists produces a lazy list that captures both arguments. |
| 207 | + - Dropping elements from a lazy list gives a safe approximation where the original list is captured in the result. In fact, it's only some suffix of the list that is retained at run time, but our modelling identifies lazy lists and their suffixes, so this additional knowledge would not be useful. |
| 208 | + |
| 209 | +Of course the function passed to `map` or `filter` could also be pure. After all, `A -> B` is a subtype of `(A -> B)^{cap}` which is the same as `A => B`. In that case, the pure function |
| 210 | +argument will _not_ show up in the result type of `map` or `filter`. For instance: |
| 211 | +```scala |
| 212 | +val xs = squares(10) |
| 213 | +val ys: LzyList[Int]^{xs} = xs.map(_ + 1) |
| 214 | +``` |
| 215 | +The type of the mapped list `ys` has only `xs` in its capture set. The actual function |
| 216 | +argument does not show up since it is pure. Likewise, if the lazy list |
| 217 | +`xs` was pure, it would not show up in any of the method results. |
| 218 | +This demonstrates that capability-based |
| 219 | +effect systems with capture checking are naturally _effect polymorphic_. |
| 220 | + |
| 221 | +This concludes our example. It's worth mentioning that an equivalent program defining and using standard, strict lists would require no capture annotations whatsoever. It would compile exactly as written now in standard Scala 3, yet one gets the capture checking for free. Essentially, `=>` already means "can capture anything" and since in a strict list side effecting operations are not retained in the result, there are no additional captures to record. A strict list could of course capture side-effecting closures in its elements but then tunnelling applies, since |
| 222 | +these elements are represented by a type variable. This means we don't need to annotate anything there either. |
| 223 | + |
| 224 | +Another possibility would be a variant of lazy lists that requires all functions passed to `map`, `filter` and other operations like it to be pure. E.g. `map` on such a list would be defined like this: |
| 225 | +```scala |
| 226 | +extension [A](xs: LzyList[A]) |
| 227 | + def map[B](f: A -> B): LzyList[B] = ... |
| 228 | +``` |
| 229 | +That variant would not require any capture annotations either. |
| 230 | + |
| 231 | +To summarize, there are two "sweet spots" of data structure design: strict lists in |
| 232 | +side-effecting or resource-aware code and lazy lists in purely functional code. |
| 233 | +Both are already correctly capture-typed without requiring any explicit annotations. Capture annotations only come into play where the semantics gets more complicated because we deal with delayed effects such as in impure lazy lists or side-effecting iterators over strict lists. This property is probably one of the greatest plus points of our approach to capture checking compared to previous techniques which tend to be more noisy. |
| 234 | + |
| 235 | +---- |
| 236 | + |
| 237 | +Next: [Capability Polymorphism](./cc-polymorphism.md) |
0 commit comments