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
Copy file name to clipboardExpand all lines: docs/_docs/reference/experimental/capture-checking/mutability.md
+5-168Lines changed: 5 additions & 168 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -75,13 +75,13 @@ an update method or an update class as non-private member or constructor.
75
75
76
76
When we create an instance of a mutable type we always add `cap` to its capture set. For instance, if class `Ref` is declared as shown previously then `new Ref(1)` has type `Ref[Int]^`.
77
77
78
-
**Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type.
78
+
**Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type. (Note: This is currently not enforced)
79
79
80
-
**Definition:** A class is _read_only_ if the following conditions are met:
80
+
**Definition:** A parent class constructor is _read-only_ if the following conditions are met:
81
81
82
-
1.It does not extend any exclusive capabilities from its environment.
83
-
2.It does not take parameters with exclusive capabilities.
84
-
3.It does not contain mutable fields, or fields that take exclusive capabilities.
82
+
1.The class does not retain any exclusive capabilities from its environment.
83
+
2.The constructor does not take arguments that retain exclusive capabilities.
84
+
3.The class does not does not have fields that retain exclusive universal capabilities.
85
85
86
86
**Restriction:** If a class or trait extends `Mutable` all its parent classes or traits must either extend `Mutable` or be read-only.
87
87
@@ -293,166 +293,3 @@ The subcapturing theory for sets is then as before, with the following additiona
293
293
-`{x, ...}.RD = {x.rd, ...}.RD`
294
294
-`{x.rd, ...} <: {x, ...}`
295
295
296
-
## Separation Checking
297
-
298
-
The idea behind separation checking is simple: We now interpret each occurrence of `cap` as a separate top capability. This includes derived syntaxes like `A^` and `B => C`. We further keep track during capture checking which capabilities are subsumed by each `cap`. If capture checking widens a capability `x` to a top capability `capᵢ`, we say `x` is _hidden_ by `capᵢ`. The rule then is that any capability hidden by a top capability `capᵢ` cannot be referenced independently or hidden in another `capⱼ` in code that can see `capᵢ`.
299
-
300
-
Here's an example:
301
-
```scala
302
-
valx:C^= y
303
-
... x ... // ok
304
-
... y ... // error
305
-
```
306
-
This principle ensures that capabilities such as `x` that have `cap` as underlying capture set are un-aliased or "fresh". Any previously existing aliases such as `y` in the code above are inaccessible as long as `x` is also visible.
307
-
308
-
Separation checking applies only to exclusive capabilities and their read-only versions. Any capability extending `SharedCapability` in its type is exempted; the following definitions and rules do not apply to them.
309
-
310
-
**Definitions:**
311
-
312
-
- The _transitive capture set_`tcs(c)` of a capability `c` with underlying capture set `C` is `c` itself, plus the transitive capture set of `C`.
313
-
314
-
- The _transitive capture set_`tcs(C)` of a capture set C is the union
315
-
of `tcs(c)` for all elements `c` of `C`.
316
-
317
-
- Two capture sets _interfere_ if one contains an exclusive capability `x` and the other also contains `x` or contains the read-only capability `x.rd`. Conversely, two capture sets are _separated_ if their transitive capture sets don't interfere.
318
-
319
-
Separation checks are applied in the following scenarios:
320
-
321
-
### Checking Applications
322
-
323
-
When checking a function application `f(e_1, ..., e_n)`, we instantiate each `cap` in a formal parameter of `f` to a fresh top capability and compare the argument types with these instantiated parameter types. We then check that the hidden set of each instantiated top capability for an argument `eᵢ` is separated from the capture sets of all the other arguments as well as from the capture sets of the function prefix and the function result. For instance a
324
-
call to
325
-
```scala
326
-
multiply(a, b, a)
327
-
```
328
-
would be rejected since `a` appears in the hidden set of the last parameter of multiply, which has type `Matrix^` and also appears in the capture set of the
329
-
first parameter.
330
-
331
-
We do not report a separation error between two sets if a formal parameter's capture set explicitly names a conflicting parameter. For instance, consider a method `seq` to apply two effectful function arguments in sequence. It can be declared as follows:
332
-
```scala
333
-
defseq(f: () =>Unit; g: () ->{cap, f} Unit):Unit=
334
-
f(); g()
335
-
```
336
-
Here, the `g` parameter explicitly mentions `f` in its potential capture set. This means that the `cap` in the same capture set would not need to hide the first argument, since it already appears explicitly in the same set. Consequently, we can pass the same function twice to `compose` without violating the separation criteria:
337
-
```scala
338
-
valr=Ref(1)
339
-
valplusOne= r.set(r.get +1)
340
-
seq(plusOne, plusOne)
341
-
```
342
-
Without the explicit mention of parameter `f` in the capture set of parameter `g` of `seq` we'd get a separation error, since the transitive capture sets of both arguments contain `r` and are therefore not separated.
343
-
344
-
### Checking Statement Sequences
345
-
346
-
When a capability `x` is used at some point in a statement sequence, we check that `{x}` is separated from the hidden sets of all previous definitions.
347
-
348
-
Example:
349
-
```scala
350
-
vala:Ref^=Ref(1)
351
-
valb:Ref^= a
352
-
valx= a.get // error
353
-
```
354
-
Here, the last line violates the separation criterion since it uses in `a.get` the capability `a`, which is hidden by the definition of `b`.
355
-
Note that this check only applies when there are explicit top capabilities in play. One could very well write
356
-
```scala
357
-
vala:Ref^=Ref(1)
358
-
valb:Ref^{a} = a
359
-
valx= a.get // ok
360
-
```
361
-
One can also drop the explicit type of `b` and leave it to be inferred. That would
362
-
not cause a separation error either.
363
-
```scala
364
-
vala:Ref^=Ref(0
365
-
valb= a
366
-
valx= a.get // ok
367
-
```
368
-
369
-
### Checking Types
370
-
371
-
When a type contains top capabilities we check that their hidden sets don't interfere with other parts of the same type.
372
-
373
-
Example:
374
-
```scala
375
-
valb: (Ref^, Ref^) = (a, a) // error
376
-
valc: (Ref^, Ref^{a}) = (a, a) // error
377
-
vald: (Ref^{a}, Ref^{a}) = (a, a) // ok
378
-
```
379
-
Here, the definition of `b` is in error since the hidden sets of the two `^`s in its type both contain `a`. Likewise, the definition of `c` is in error since the hidden set of the `^` in its type contains `a`, which is also part of a capture set somewhere else in the type. On the other hand, the definition of `d` is legal since there are no hidden sets to check.
380
-
381
-
### Checking Return Types
382
-
383
-
When a `cap` appears in the return type of a function it means a "fresh" top capability, different from what is known at the call site. Separation checking makes sure this is the case. For instance, the following is OK:
384
-
```scala
385
-
defnewRef():Ref^=Ref(1)
386
-
```
387
-
And so is this:
388
-
```scala
389
-
defnewRef():Ref^=
390
-
vala=Ref(1)
391
-
a
392
-
```
393
-
But the next definitions would cause a separation error:
394
-
```scala
395
-
vala=Ref(1)
396
-
defnewRef():Ref^= a // error
397
-
```
398
-
The rule is that the hidden set of a fresh cap in a return type cannot reference exclusive or read-only capabilities defined outside of the function. What about parameters? Here's another illegal version:
399
-
```scala
400
-
defincr(a: Ref^):Ref^=
401
-
a.set(a.get +1)
402
-
a
403
-
```
404
-
These needs to be rejected because otherwise we could have set up the following bad example:
405
-
```scala
406
-
vala=Ref(1)
407
-
valb:Ref^= incr(a)
408
-
```
409
-
Here, `b` aliases `a` but does not hide it. If we referred to `a` afterwards we would be surprised to see that the reference has now a value of 2.
410
-
Therefore, parameters cannot appear in the hidden sets of fresh result caps either, at least not in general. An exception to this rule is described in the next section.
411
-
412
-
### Consume Parameters
413
-
414
-
Returning parameters in fresh result caps is safe if the actual argument to the parameter is not used afterwards. We can signal and enforce this pattern by adding a `consume` modifier to a parameter. With that new soft modifier, the following variant of `incr` is legal:
415
-
```scala
416
-
defincr(consume a: Ref^):Ref^=
417
-
a.set(a.get +1)
418
-
a
419
-
```
420
-
Here, we increment the value of a reference and then return the same reference while enforcing the condition that the original reference cannot be used afterwards. Then the following is legal:
421
-
```scala
422
-
vala1=Ref(1)
423
-
vala2= incr(a1)
424
-
vala3= incr(a2)
425
-
println(a3)
426
-
```
427
-
Each reference `aᵢ` is unused after it is passed to `incr`. But the following continuation of that sequence would be in error:
428
-
```scala
429
-
vala4= println(a2) // error
430
-
vala5= incr(a1) // error
431
-
```
432
-
In both of these assignments we use a capability that was consumed in an argument
433
-
of a previous application.
434
-
435
-
Consume parameters enforce linear access to resources. This can be very useful. As an example, consider Scala's buffers such as `ListBuffer` or `ArrayBuffer`. We can treat these buffers as if they were purely functional, if we can enforce linear access.
436
-
437
-
For instance, we can define a function `linearAdd` that adds elements to buffers in-place without violating referential transparency:
`linearAdd` returns a fresh buffer resulting from appending `elem` to `buf`. It overwrites `buf`, but that's OK since the `consume` modifier on `buf` ensures that the argument is not used after the call.
443
-
444
-
### Consume Methods
445
-
446
-
Buffers in Scala's standard library use a single-argument method `+=` instead of a two argument global function like `linearAdd`. We can enforce linearity in this case by adding the `consume` modifier to the method itself.
447
-
```scala
448
-
classBuffer[T] extendsMutable:
449
-
consume def+=(x: T):Buffer[T]^=this// ok
450
-
```
451
-
`consume` on a method implies `update`, so there's no need to label `+=` separately as an update method. Then we can write
452
-
```scala
453
-
valb=Buffer[Int]() +=1+=2
454
-
valc= b +=3
455
-
// b cannot be used from here
456
-
```
457
-
This code is equivalent to functional append with `+`, and is at the same time more efficient since it re-uses the storage of the argument buffer.
0 commit comments