Changes to Mutable

[odersky]

1. Mutable and ExclsuiveCapability are not longer classifiers. This means Mutable classes can capture other capabilities. Read is still a classifier.

2. Update methods in nested classes can access exclusive capabilities external to enclosing classes.

[Linyxus]

I am playing with this PR, and found the following code compile:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Logger extends SharedCapability, Mutable:  // (1) does this make sense?
  private var _state: Int = 0
  update def log(msg: String): Unit = ()
def onlyShared(x: Object^{cap.only[SharedCapability]}): Unit = ()
def main(): Unit =
  onlyShared(Logger())  // even if we allow (1), why would this type check?
  val t: Logger^{} = Logger()  // and this type checks too, thus the above line I guess

• We have a Logger that extends both SharedCapability and Mutable. Does it make sense? If "shared" means can be safely exempted from separation checking, this feels conflicting.
• The last line seems to be a bug. Logger extends Mutable, has a mutable field, and an update method, yet its instance is pure.

[odersky]

We currently have deep problems with Mutables carrying the empty capture set. I am trying to fix them but it turns out it's not easy.

Also, no probably combining SharedCapability and Mutable should be forbidden.

[Linyxus]

Another example:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Logger extends SharedCapability:
  def log(msg: String): Unit = ()
class TracedRef(logger: Logger^{cap.only[SharedCapability]}) extends Mutable:
  private var _data: Int = 0
  update def set(newValue: Int): Unit =
    logger.log("set")
    _data = newValue
  def get: Int =
    logger.log("get")  // error, but should it be allowed?
    _data

Right now using a shared capability in a non-update method inside a Mutable class is disallowed. Again, if "shared" means "we don't care about them in separation checking", should it also be exempted?

[natsukagami]

Right now using a shared capability in a non-update method inside a Mutable class is disallowed. Again, if "shared" means "we don't care about them in separation checking", should it also be exempted?

This might be conflicting, since it would mean a TracedRef^{caps.only[Read]} would actually capture the logger, even though Read and SharedCapability have no relationship on the classifier tree.

However from a practical point of view I agree we should exempt this case