Le’t’s say we have a Run trait that abstracts over the notion of running a given task, as well was a helper class, Tasks, that aggregates a bunch of tasks and knows how to run them:
trait Run:
def run(taskId: String): Unit
case class Tasks(taskIds: List[String]):
def runAll(runner: Run): Unit =
taskIds.foreach(runner.run)
Later, somebody defines a straightforward Print capability:
trait Print extends SharedCapability:
def println(str: String): Unit
We can then reasonably write a Run that depends on Print to print task identifiers:
Armed with all that, it should be easy to take a Tasks and run it through that printRunner:
def printAll(tasks: Tasks)(using Print): Unit =
tasks.runAll(printRunner)
This won’t compile, because runAll takes a non-capturing Run, and printRunner captures its Print.
The only way I can think to “fix” this is by rewriting Tasks.runAll to take a Run^ (or, equivalently, to make Run a capability). But this feels like the wrong way around: Tasks.runAll doesn’t care about tracking, since it doesn’t capture its runner. And yet it must explicitly declare Run as tracked?
Am I missing something, is there maybe a better way of “fixing” the problem? Or is the design wrong, even though it seems fairly reasonable?
My thoughts were that some kind of existential capture set might, erm, capture what you’re after.
A quick Google AI search implies there is such a thing, and mentioned ‘System Capless’ (do I need to write a trademark sign here?).
Being a grug, I didn’t check to see if Gemini was making ‘forward-looking statements’; I haven’t even read the System F stuff or the other formal thing that Scala 3 is based for that matter.
If you can see anything useful from up there in your U2, let us folks in the lower troposphere know…
That’s sort of the point though. Imagine runAll is in a different library, one that I’m not the maintainer of. If the author hasn’t thought about capture checking for a function that doesn’t care about capture checking, I can’t call it.
If runAll in a different library that was not compiled with capture checking on, you can still call it. We use lenient type checking at the boundary between capture checked and non-capture checked.
I more meant: if runAll is in a different library, compiled with capture checking, but doesn’t include capture checking annotations because it doesn’t really need one at implementation site, then I, at call site, might not be able to call it.
I worry this means that if you want your library code to be generally useful, you need to annotate everything, all the time, with capture checking instructions.
Is there any other way it could possibly work, though?
People get upset fighting the borrow checker in Rust because it checks everything, even when you wish it wouldn’t. Why? Because checking everything is the only way to give actual guarantees. Without actual guarantees, degree of partial guarantee degrades rapidly when you compose code.
So I don’t really see how there’s a useful intermediate between “I really did not think about this–you’re on your own” and “yes, I thought this aspect through”. Maybe “I annotated the part I thought through, either way, and the parts I didn’t annotate are not thought through”?
So you would like, perhaps, an option at least for capture checking to be strongly or weakly typed on a method-by-method basis rather than by compilation unit?
I don’t think that’s what I want, but I’m also not quite sure what I want. I’m merely pointing out that when writing a “capture checking enabled” library, every function that doesn’t allow its arguments to escape must be rewritten:
def foo(bar: Bar, baz: Baz) =
println(s"$bar: $baz")
// to:
def foo[c1^, c2^](bar: Bar^{c1}, baz: Baz^{c2}) =
println(s"$bar: $baz")
The syntactic cost is really quite heavy, and a little different from the general discourse, which is that capture checking won’t actually change much except when you do something wrong (also, in this particular context, is there really an advantage to that over having Bar^ and Baz^?)
The problem is sorted for function types, since the way one would naturally write Scala code is exactly the way you do work around the “problem:
// An actual argument for `f` may me tracked or not, both are valid.
def foo2(f: Bar => Baz) = ...
I realise it’s not possible to do the exact same thing for non-function types - there’s no syntax I can think of that’d be the value equivalent to A → B - but it’s true that in my experience, assuming functions to be tracked works out really smoothly (which may just be that I have yet to encounter the “bad” cases) while assuming non-functions to be pure leads to, well, this discussion. Suddenly we must learn to default to a different syntax than the one we’ve learned for declaring non-function types.
I also want to make it clear that I’m not being critical or ungrateful of the work done. This is intended as a return of experience, possibly highlighting some quality of life issues, not as a put down of the team’s hard work. I apologise if it came of that way.
Actually, parameterization is overkill here. You need that only if you want to correlate two capture sets (such as the one for the argument and the one for the result). So, if you just want to allow arbitrary retained sets in Bar and Baz, you should write foo like this:
But, I would argue it’s actually quite rare that you need this. In this example Bar and Baz are data to be printed. Good design would suggest that data is pure, and does not come with latent effects or capabilities.
To me this suggests that in the initial example Run should indeed have been defined as trait Run extends SharedCapability, because Run does not represent pure data but the effect of running a task. Do I understand this correctly?
I think that’s the root of the problem, and it’s probably me using capture checking in a way that is not intended.
In my mind, capture checking is the ability to prevent values from escaping when that’s dangerous. It’s a superset of what you seem to have in mind: the ability to prevent capabilities from escaping.
An example of a value that is not a capability and we might want to track is a secret - you may recall from our live-coding last year in Krakow, a Secret that should only be available in the scope of a withSecret[A](f: Secret => A): A function to guarantee that it does not leak (typically for handshakes with secret auth providers).
With your view of capture checking, I do agree this is less of an issue. foo as I wrote it declares that it only takes non-effectful values, which is more reasonable than having to declare an argument as tracked when you don’t want to capture it.
I can’t help but feel it’s a little unfortunate to limit capture checking to a subset of the problems it could solve, but am also well aware that, not being in the trenches, I lack a lot of context and my opinion is ill-informed.
