Capture checking being confusing again

Question
1

I’m, once again, very confused by some capture checking behaviour, which I feel might be a bug.

In the following code, I try to model a Rand capability based on a State one:

//> using scala 3.nightly
//> using option -language:experimental.captureChecking -nowarn

import caps.*

trait State[A] extends SharedCapability:
  def get: A
  def set(a: A): Unit

def get[A]: State[A] ?-> A          = s ?=> s.get
def set[A](a: A): State[A] ?-> Unit = s ?=> s.set(a)

trait Rand extends SharedCapability:
  def range(min: Int, max: Int): Int

object rand:
  def fromState: (s: State[Long]) ?-> Rand^{s} =
    new Rand:
      override def range(min: Int, max: Int) =
        val seed             = get
        val (nextSeed, next) = (seed + 1, seed.toInt) // obviously wrong, but not the point...
        set(nextSeed)
        next

This fails with:

[error] Found:    rep$_.this.Rand^{rep$_.this, s, cap}
[error] Required: rep$_.this.Rand^{s}
[error] 
[error] Note that capability rep$_.this is not included in capture set {s}.
[error] 
[error] where:    cap is a fresh root capability classified as SharedCapability created in anonymous function of type (using s²: rep$_.this.State[Long]): rep$_.this.Rand^{s²} when constructing Capability instance Object with rep$_.this.Rand^ {...}
[error]         next
[error]             ^

And I don’t understand:

  • why do I need to capture cap ? I suspect there’s two cap involved here, the one captured by Rand and the one captured by State, but surely they’re both captured here? One because, well, it’s a Rand, and the second because it captures s: State and therefore that cap by transitivity?

  • what’s rep$_.this? I’m assuming it’s the State syntethised by automatic conversion to context function, and this specific part of the error disappears if I declare that State explicitly, but why do I need to do that?

2

It’s because Rand extends SharedCapability. Any newly created capability object gets a fresh cap associated with it, to express that we are creating a fresh capability. If we did not do that, and the capability did not capture anything else (like the s in your example) we would end up with a pure value of a capability class which would be a contradiction in terms. If you declare Randas a regular class, the example compiles. There’s then still a warning about a redundant capture that might be spurious. I’ll follow up on that.

1 Like
3

Ooof…

First, thanks a lot for that answer. And yes, simply declaring fromState as:

def fromState: (s: State[Long]) ?-> Rand^{s, cap} = ...

fixes the test case (even the weird rep$_.this part).

But as a non-expert user, I have to admit that having multiple things called cap, and understanding which cap is implicitly captured and which needs to be explicitly declared, and how they differ… Everything else about capture checking feels reasonable and logical, but this might take a little while for “regular” developers to get their head around. It’s certainly taking me a while :slight_smile:

Here, for example: I’m assuming that Rand being a SharedCapability implies all values of type Rand capture “some” cap, and therefore that I do not need to declare it in the return value of fromState. However, s also captures some other cap - so we have 2 caps. Which one is the one I declared in Rand^{s, cap}?

  • the one that comes from Rand being a SharedCapability? Then why do I need to declare that, since this is still a Rand?
  • the one that’s captured by s? Then why do I need to declare that, since it’s transitively captured by s?
  • some third cap?

I’m in no way questioning the need for such a behaviour, merely pointing out that from a user perspective, it’s slightly confusing in its current shape…

4 Likes
4

I think you have hit a real problem here – adding cap silently to new instances of capability classs is indeed confusing! I have given this some more thought and now believe that there’s no need to do this if we are a bit more precise elsewhere.

I implemented this in Don't add cap when creating instances of capability classes. by odersky · Pull Request #24256 · scala/scala3 · GitHub . That should hopefully avoid this particular source of confusion.

2 Likes
5

I’ve run this code in Scala 3.7.3 and got it to work.

  1. You construct a concrete capability instance s: State[Long]. This is the authority to read and update a Long seed.
  2. rand.fromState(using s)
  • Satisfies the context function (s: State[Long]) ?-> ... by passing s implicitly.
  • Inside fromState, the literal s ?=> new Rand { ... } binds that same capability into the closure.
  • Return type is Rand^{s}, so the type tracks that the rng value is tied to the lifetime of s.
  1. rng.range(0, 10)
  • When you call range, it executes the body that uses get[Long] and set(...).
  • Those methods require a State[Long] capability, which is not provided by the call site now; it is already captured by the closure created in fromState. In other words, range runs with access to s that was captured earlier.
  1. get[Long](using s)
  • This is a direct call to the capability function, bypassing Rand. It proves the seed advanced to 45 after three calls, matching the increments done inside range.
import scala.language.experimental.captureChecking
import scala.caps.*

object SharedCapExperiment:
  trait State[A] extends Sharable:
    def get: A
    def set(a: A): Unit

  def get[A]: State[A] ?-> A = s ?=> s.get
  def set[A](a: A): State[A] ?-> Unit = s ?=> s.set(a)

  trait Rand:
    def range(min: Int, max: Int): Int

  object Rand:
    def fromState: (s: State[Long]) ?-> Rand^{s} =
      s ?=> new Rand:
        override def range(min: Int, max: Int): Int =
          val seed = get[Long]
          val nextSeed = seed + 1
          set(nextSeed)
          seed.toInt


  @main def runSharedCapExperiment(args: String*): Unit =
    println("File /Users/drmark/IdeaProjects/PLANE/src/main/scala/FPIntro/SharedCapExperiment.scala created at time 4:27PM")
    val s: State[Long] = new State[Long]:
      private var x = 42L

      def get: Long = x

      def set(a: Long): Unit = x = a

    // Build a Rand that captures the capability s
    val rng: Rand^{s} = Rand.fromState(using s) // type inferred: Rand^{s}

    // Use it a few times
    println(rng.range(0, 10)) // e.g. 2  (42 % 10)
    println(rng.range(0, 10)) // e.g. 3  (43 % 10)
    println(rng.range(0, 10)) // e.g. 4  (44 % 10)

    // You can also inspect the raw state directly via the capability
    val currentSeed = get[Long](using s)
    println(s"raw seed now = $currentSeed") // should be 45 here