Confusing capture checking error

Question
1

I’m a little confused by the following example using capture checking:

trait FileSystem extends Capability:
  def print(msg: String): Unit

class Logger(using fs: FileSystem):
    def info(msg: String): Unit = fs.print(msg)

def log(msg: String): FileSystem ?-> Unit =
  val l = new Logger
  l.info(msg)

This fails to compile with the following slightly sybiline error message:

[error] reference (Logger.this.fs : Capture$_.this.FileSystem^) is not included in the allowed capture set {}
[error] of an enclosing function literal with expected type (fs: Capture$_.this.FileSystem^) ?-> Unit^{fs}
[error]   l.info(msg)
[error]   ^^^^^^^^^^^

My intuition was to make log 's return type (fs: FileSystem) ?-> Unit^{fs} , but this still fails with an additional warning, that Unit already captures fs.

Also I was expecting to be allowed to write (fs: FileSystem) ?->{fs} Unit , but that results in a parse error.

I suspect I’m missing a rule to do with the way the way capture sets are handled in method calls, but I can’t seem to find anything in the documentation…

2

Hi,

The following will work:

//> using scala 3.nightly
import language.experimental.captureChecking
import caps.*

trait FileSystem extends Capability:
  def print(msg: String): Unit

class Logger(using fs: FileSystem^): 
//.                    ^^^^^^^^^^ tracked capabilities must be qualified with a hat or capture set
  def info(msg: String): Unit = fs.print(msg)

def log(msg: String): (fs: FileSystem^) ?-> Unit =
//                         ^^^^^^^^^^^ same here
  val l = new Logger
  l.info(msg)

@main def run =
   given (FileSystem^) = new FileSystem { def print(m: String) = println(m) }
   log("hi")

Tracked capabilities (those types extending from Capability) require a hat or capture set on them.
Otherwise, the type system cannot keep track of their uses.

Edit: the initial example should compile just fine on 3.nightly.

This is wrong, because it specifies that the result of the function captures fs, but
it is the function itself that makes use of it. Generally, a capture annotation on a non-tracked base type like Unit or Int is not necessary, because such values cannot capture anything.

The correct type is (fs: FileSystem^) ?-> Unit. Since the fs is passed as a parameter, we expect that the function can potentially use it already.

A type like (fs: FileSystem) ?->{fs} Unit really desugars into (FileSystem ?-> Unit)^{fs} which by lexical scoping is wrong (there is no fs). Note that captures are not like effects in a traditional effect system. A function (x: A) ->^C B does not mean “if I supply an A, then C happens (which may depend on the argument x) and I get a B back”. It’s rather “this is a function capturing things in C and I can pass it an A and get a B back”.

hth

-Oliver

1 Like
3

Thank you so much for taking the time to reply. It definitely helps (and it does fix my problem).

First, yeah, I should probably have tried the latest nightly - it didn’t fix the error, but it certainly made the error message more understandable (also, your fix doesn’t actually work under 3.6.4, so I could have looked a good long time…).

Second, I’m actually a little surprised that I need the ^ on FileSystem. I thought the entire point of having it extend Capability was that it basically always had a ^, as far as the compiler was concerned? Also, if I remove the ^ in both places it’s tacked on to FileSystem, things seem to work again, so I’m a little confused here.

As for the last bit - the ?->{...}, I was getting a parse error, not a type error, so I thought maybe there was an issue with the parser. Whatever the case might have been however, I can’t reproduce using the latest nightly, so it’s all good.

Thanks again for your help and clear answers.

Nicolas

1 Like
4

Ah yes, my bad! The original example compiles as-is on nightly. It is possible to omit the hat if it is a type directly inheriting from Capability, but types that do not and capture some capabilities will sometimes need a capture annotation. I got hung up on the problem with the implicit function arrow and ended up adding hats everywhere explicitly.

5

That makes sense, thank you. Again, I appreciate your time on this (and am having quite a bit of fun with capture checking!)

1 Like