Experimental Capture Checking: New Syntax for Explicit Capture Polymorphism

[renghen-marideal]

Nim has a nice syntax for allowing and forbidding effects, which I hope I am not wrong is quite close to what capabilities offer.

https://nim-lang.org/docs/manual.html#effect-system-tag-tracking

[sjrd]

On the topic of terseness. Overall, a good decision criteria for how terse syntax should be is how often it is expected to be used.

• + needs to be short because we use it all the time. The fact that is “obscure” (if you don’t know math) is not a big deal because you are going to see very early and very often. So you will learn it quickly and it will enter your efficient, unconscious long-term memory. The visual terseness will then help you by minimizing the processing power required to access your efficient memory.
• transparent can be long because we almost never use it. It is good that is spelled out completely, because many users will almost never see it, if at all. Therefore, it will not enter anyone’s efficient long-term memory. That means we need to use our active, inefficient processing power to understand it. It therefore needs to be long to help your brain makes sense of it, despite the fact it’s not in your efficient memory.

If we expect cap/^ to be rarely written out in practice, as is the initial post suggests:

@etaconversion

However, we expect explicit polymorphism for captures to be fairly rare in practice, […]

then I suggest making it even longer than cap. If it is truly rare, it should be pretty long and self-descriptive, perhaps as long as capability.

I understand that doesn’t look good in papers. In a paper about capture checking, we expect explicit capture annotations to be very frequent! So it makes sense for papers to want short syntax for them. But that’s OK! Papers and actual languages don’t need to use the same syntax. They usually don’t.

[daniel-ciocirlan]

I echo every one of @jducoeur’s concerns:

What does this look like in documentation to naive users?

The syntax should explain itself. The less explanation is needed to justify the syntax, the better the syntax, and conversely. I think the current syntax needs lots of explanation.

How do we teach this?

As much as I personally try to mitigate this with my work at Rock the JVM, Scala is currently perceived to be hard to learn. We should really strive to not make things worse.

We should aim to make capture checking teachable within 30 minutes.

As it stands, this syntax will need piles of articles and tutorials for anyone to even take a stab at it. I have no problem making all these materials, but it’s a disservice to the language. The Reddit reaction is informative: if users say “wtf” or “this is just for nerds”, we’re losing them.

Are we choosing the right level for the keyword? I’m realizing that cap reminds me of implicit in a very specific way: we’re talking about the mechanism being expressed (“capture”).

The keywords/keytokens should add clarity and describe intent. I believe implicit was badly perceived because the intent was unclear and therefore misinterpreted and misused. Same danger with cap.

---

Scala is safety + convenience. In its current form, capture checking is +100 safety, -100 convenience. At a time when Scala badly needs to be seen as convenient and friendly, we need a better tradeoff. At a minimum, we should not deduct convenience points.

Some suggestions:

• None of this should be visible to beginners, because it will scare them off.
• Everything should be opt-in - people should enable this when they’re ready, because it will complicate their codebases, for good reason.
• Nothing less than excellent docs are acceptable for this massive change.

My take:

• The words “captured”, “managed”, “tracked” or even “resource” better describe meaning.
• I’d use a proper type name “Cap” or even “AnyCap” for the mother of all capabilities, and it would help disambiguate.
• I concur with @lchoran in that the ^ should act like a warning. I’d either use a known symbol for that (for example !) or a proper word like “tracking”.
• Curly braces look off, because their current meaning is “scope”. Square braces would IMO work better because they live in the mental space for types.

[etaconversion]

@Ichoran

Sure, a capture set is an upper bound, but so is a trait: you can potentially call any of its methods, but you don’t have to call any. The way it’s phrased here the natural parallel–and I think it’s important to form the parallel because if there is one it will help people learn about it!–is: […]

We need to consider capturing types T^C as a whole and not just capture sets. The T type describes the power the value has (which corresponds to the intersection view), and the C part expresses a tracking obligation (what such a T value can at most do resp. what it is derived from). Obligations are subject to subcapturing, which subsumes set inclusion (the union view).

The most powerful capability is of type Nothing^{}: it can do anything, and we do not have any obligations to track it. Dually, Any^{cap} is the most restricted capability type: we can do nothing with it, and are obligated to track it everywhere it occurs in types. (This perspective was proposed by @Linyxus)

If we have an expression of type T^C then its result value (if the expression terminates) will capture no more capabilities than mentioned in the set C. And that doesn’t necessarily coincide with the capabilities that were used to compute the result:

import language.experimental.captureChecking
import caps.*

class Logger:
  def log(s: String): Unit = ()

trait X extends Capability {def x: String }
trait Y extends Capability {def y: String } 

@main
def test: Unit =
  val x: X^ = new X { def x = "x" }
  val y: Y^ = new Y { def y = "y" }

  def foo(w: Logger^{x,y}): () -> Unit =
      w.log("hi"); { () => () }

  def bar(w: Logger^{x,y}): () ->{w} Unit =
      w.log("hi"); { () => w.log("again") }

  val foox: (w: Logger^{x,y}) -> (() -> Unit) = foo
                               //      ^ w not captured by result              
  val barx: (w: Logger^{x,y}) -> (() ->{w} Unit) = bar

  val loggerx: Logger^{x} = new Logger { override def log(s: String): Unit = {x.x : Unit } }
  val loggery: Logger^{y} = new Logger { override def log(s: String): Unit = {y.y : Unit } }
  val loggerxy: Logger^{x,y} = loggerx // ok
  val loggerPure: Logger = loggerx // error: would loose track of x

  // these are all ok
  foo(loggerx)
  foo(loggery)  
  foo(loggerxy) 
  bar(loggerx)
  bar(loggery)
  bar(loggerxy)

We let X and Y extend Capability, which means that all variables of those types must be tracked throughout the type system. If some value captures them (a prerequisite to potentially using them), then the value is obligated to mention them in its capture set. As can be seen with the logger values above, the type system obligates us to track x and y in them, which makes loggerx and loggery themselves trackable resources. Both have the power of the Logger type but different obligations.

As another example, say we have () => loggerx.log("x"), then the most precise type we can give the function is () ->{loggerx} Unit. The function has the power to produce a Unit value and is obligated to track loggerx, which transitively means it is also obligated to track x due to loggerx’s type. Ergo: () ->{loggerx} Unit <: () ->{x} Unit. By set inclusion, both are subtypes of () ->{loggerx,x} Unit.

Btw, another very useful perspective on capture sets is thinking of them as the part of the context of named capabilities that is relevant for a value, which also tells us the part of the context that is irrelevant. loggerx doesn’t care about y, and we could remove y from the context if we continue only using loggerx.
Respectively we could distribute loggerx and loggery safely between two threads, etc… We have thus a means for reasoning about separation of capabilities in the types, which leads to Rust-style usage patterns (shameless plug for how such as system could look like: https://bracevac.org/assets/pdf/reachability.pdf https://bracevac.org/assets/pdf/popl24.pdf https://bracevac.org/assets/pdf/oopsla23.pdf)
Something along those lines is already brewing in the capture checker, but we are not ready to talk about it yet.

@Ichoran

Regarding tunneling […]

If a trait is generic over regular type variables, that must include all types, including capturing and non-capturing types. For that to work, we have to suspend the capturing types passed to a generic type parameter in a “box” type. This technique enabled us to retrofit the standard collections library with capture checking after very minimal adjustments.

@Ichoran

trait Hey[-A, +C] {
  def ac(a: A): C
}

you can tell that any capabilities that appear in C that aren’t in A must have been stored internally, but you can’t tell whether any capabilities in A were in fact stored for internal use or simply discarded or passed on to C; and you can’t tell whether C capabilities that appear in A were passed on or not.

We can’t tell that in such a trait due to being fully generic. To model such relationships, you’d need to add extra cap parameters for A and C, i.e., design the trait around capturing types and not regular types from the get go.

But let’s not stray too much off-topic. I’m happy to discuss more in a separate thread.

[markehammons]

@daniel-ciocirlan

We should aim to make capture checking teachable within 30 minutes.

As it stands, this syntax will need piles of articles and tutorials for anyone to even take a stab at it. I have no problem making all these materials, but it’s a disservice to the language. The Reddit reaction is informative: if users say “wtf” or “this is just for nerds”, we’re losing them.

Is the borrow checker from Rust actually teachable in 30 minutes? I don’t believe it is, but it’s unquestionably a good feature that has elevated Rust. I think we should be honest that this feature is not going to be easy to teach, but will still have significant benefits.

With regards to the reddit thread, my comment has the highest vote count, exceeding the vote count of the original comment that states

Maybe this is why peeps say Scala is complicated. This article is only for language geeks.

What should be instructional in this isn’t that capture checking being hard is bad, but rather that the case for capture checking has not been well communicated, and perhaps that communicating the use case of a feature should be given more focus when developing a feature like this. The Scala 3 Reference speaks about how to use capture checking, and its features, but it doesn’t provide a strong and easy to understand explanation of why it should exist.

[etaconversion]

Quite a bit of engagement here, very nice!

Modifiers?

@JD557

On the topic of cap being a type modifier, will it be possible to mix it with other type modifiers (e.g. opaque cap type)?

Definitely! They can have all the modifiers a regular type member could have.

What We Can Learn from Higher-Kinded Types

After some deliberation and internal discussion, we found that

@Odomontois

If yes, I like the

type C^
type D^

It has some similarity with the [] after the type to designate the kind.

is actually quite a good and logical way to think about capture parameters. Just as post-fix brackets designate a higher-kinded type parameter, so can a post-fix ^ designate a “capture-kinded” parameter. Due to the technical constraints outlined earlier, we cannot have general type-level functions working on these kinds, though.

Since the cap ^ symbol is to be used pervasively to mark tracked capabilities, it should be familiar enough to communicate what C^ ranges over.

Consequently, we should have similar expectations for notations compared to higher-kinded type parameters:

def foo[C^, D^ <: C, E <: C]() = ...
//                   ^
//     necessarily a capture variable due to its bound

trait Foo[T <: List[() ->{C} Unit], C^]:
  type D^ <: C
  type E  <: C

That also implies we when we can drop braces (or whatever delimiters) for literal capture sets: when it’s a reference to a single capture-set parameter:

type D^ <: {C}
type D^ <: C

Here, we have the problem of ambiguity between type- and and term-variable names:

trait Foo[io^]
  val io: Any^
  type C^ <: {io} // ambiguous
  type D^ <: io   // unambiguously the type-level io name

That’s bad style and should result in a warning at the very least.

But overall, this is where it’s currently headed design-wise.

Capture-Set Literals

As for capture-set literals, I’m not entirely convinced that braces are bad. It’s how we commonly write down mathematical sets. The risk of confusing them with refinements and structural types is also low because of what we write between the braces. I can’t think of any other type of delimiters that would immediately tell me: “Yes, this is a unordered, automatically de-duplicated collection of capabilities”.

Collection literals have entered the chat…

Dedicated Capture-Set Parameter Lists?

Regarding dedicated parameter lists:

@Sporarum

@etaconversion

To satisfactorily support dedicated cap-parameter lists, we need to generalize to curried class-parameter lists.

This is something we should support either way, as it already would have uses now:

class Foo[A <: { type M }](a: A)[B <: a.M]

It of course opens a whole can of worms, but I believe it to be worthwhile

A can of worms they are indeed! Which is why we are not planning to support them for the time being. However, since capture-set parameters should be erased when capture-checking is turned off, we propose grouping them at the end of type-parameter lists by convention.

Is This Like given/using?

given/using each have a very specific and unambiguous purpose. But I do not see it for capture-set parameters. We have too many degrees of freedom to put them to use, so I’m hard-pressed to identify a word that is more fitting than cap or the longer capability. For example, trait Foo[cap C] {} does nothing interesting with its capture-set parameter, and the parameter C’s existence doesn’t necessarily mean that Foo[C] instances will capture C! That depends very much on the concrete implementations of Foo.

That makes me want to double down on the post-fix hat instead of a modifier/keyword.

How Will the Docs Look Like?

We’re aiming for two complementary views in Scaladoc for capture checking enabled/disabled. Hats or any other “esoteric” tokens will not be visible by default unless demanded.

Teaching, Reddit, etc.

To the best of my knowledge, neither I nor anyone else on the team pretends this is ready for primetime. We are making steady progress and will signal once this is at a stage where a broader audience can play with it. We will of course improve error messages and the docs (there’s lots of interesting stuff in terms of mutation tracking in the pipeline we can’t wait to share).

[scalavision]

I hope this will be an amazing addition to the language.

I am also concerned about teaching this and it’s essential that there is a strategy not only on the syntax, but also how it will involve different kind of programmers.

I work mostly with java / kotlin developers trying to introduce scala every now and then.

I think newcomers and everyday programmers should not need to learn the details, the compiler should tell exactly what needs to be done if something is missing when calling a function or similar.

Library authors etc will need to learn it if they choose to use it and that’s ok.

Therefore I think ^ is the best option. It’s really easy to read and really easy to ignore if you don’t need to deal with the details, just fill in the gaps.

I have worked a lot in python and with domain experts that also are programmers. If there are good docs explaining how to use the library, it should be enough, and no need to know the inner working of capabilities.

In my experience they only want to get the work done and don’t care too much about the details.

Personally I think this is a really nice addon to the language, also the work on Scala 3 has been really successful so far, so I am excited about this. Also excited to what it could mean to scala native.

[beyondpie]

@daniel-ciocirlan

• Everything should be opt-in - people should enable this when they’re ready, because it will complicate their codebases, for good reason.

As a new comer, this is what I really hope. The feature looks very promising, but also scares me a lot. It would take me two or more years to digest the information and use it in my application, I guess…

[lihaoyi]

I’m going to echo some of the sentiments here and say that it’s too early to decide on the syntax when we do not have a good user-facing tutorial to demonstrate the use cases where this feature is expected to be applied.

This is solvable, but it needs to be done correctly.

1. First write a tutorial explaining the feature that you can post on Reddit and get random Scala users to understand.

2. After we have some common understanding, and common understandability, we can start tweaking the syntax to optimize it.

But there’s no point trying to do (2) if we do not have (1). If we can’t explain this feature in a way that people can understand, then it doesn’t really matter what the syntax is

Many person-years are going into implementing this feature, so presumably spending a few person-days or person-weeks properly explaining it to the community is a worthwhile use of time

[odersky]

@lihaoyi

I’m going to echo some of the sentiments here and say that it’s too early to decide on the syntax when we do not have a good user-facing tutorial to demonstrate the use cases where this feature is expected to be applied.

Correct. But we are not deciding on the final syntax yet. In fact, we are still very far from this stage. The discussion here is what the first strawman syntax could be for a feature that is totally research and experimental. We could decide on that behind closed doors, after all, we can change the syntax at any time or drop it entirely.

But syntax matters, even if this is only for research papers at the moment. It’s always awkward and costly to change it afterwards. So we thought getting community feedback early could help improving the initial proposals, and looking at this thread I have the impression that goal was achieved.

[Ichoran]

@etaconversion

We need to consider capturing types T^C as a whole and not just capture sets. The T type describes the power the value has (which corresponds to the intersection view), and the C part expresses a tracking obligation (what such a T value can at most do resp. what it is derived from).

Thanks; I had understood the above, but the example is helpful in seeing how that plays out.

I’m trying to implement the same functionality with existing constructs plus manual boilerplate as a way to understand whether existing concepts map well enough so that they should be used (and probably also guide syntax).

I’m not done–and I’m not sure I’ll have time to finish in any case–but I’ve already run into two cases that make me wonder about the existing scheme somewhat.

Firstly, that you get the ability to be tracked from the permission to capture anything seems a bit weird. For instance, consider these two cases:

val x: X^ = new X { def x = "x" }
val y1: Y^ = new Y { def y = "y" }
val y2: Y^ = new Y { def y = x.x }
val y3: Y^ = new Y { def y = y1.y }

We presumably don’t want y2 to be able to capture x because X is tracked. So we can’t interpret Y^ as Y^{cap} here; that clearly is too much power.

But y3 also seems wrong–shouldn’t we have to know when we capture something tracked even if it’s another instance of our own type? So we also can’t interpret it as Y^{Y}.

In fact, it seems like we should have been allowed to capture nothing, so Y^ in these cases should be interpreted as Y^{}, i.e. we were not allowed to capture anything: we are just ourselves. But that also can’t be right because if y1: Y^{a} then {y1} <: {a}. But it’s not right that {y1} <: {} because clearly if you can’t capture anything you shouldn’t be able to capture y1.

Perhaps y1: Y^ has to mean y1: Y^{y1}? I captured myself? That does seem to work, as far as I can tell.

Regardless, something seems off to me, at least in collapsing the idea of capture sets and tracked classes and authority going back to caps.cap. Maybe this is the right level of generality, and I think it is self-consistent as far as it goes; but I’m not sure that it goes quite where one would want or expect, at least as described.

Secondly, there’s an issue of multiple captures of the same type, but I’ll save that for later (and maybe once the first one is clear the second will also magically resolve).

[Ichoran]

Here’s a working prototype of using a lot of manual boilerplate and opaque types to produce very similar rules to capture checking as described.

It does so by producing a parallel type universe with a lower and upper bound (all actually just opaque types of Unit) where (1) new tracked types define their own pair of bounds, and (2) new tracked instances define a single type within the bounds they are known to exist in.

Because we can have infix opaque type ^ the syntax kind of matches; the main difference is that you have to use hand-generated boilerplate like x_cap.Type instead of simply x in capture sets; and you build sets with (a & b & C) not {a, b, C}.

And of course it does not do capture checking. It has no machinery to detect when a capture occurs! It just keeps track of types. Here it is: Scastie - An interactive playground for Scala.

It does make me wonder about the whole capture set notation, though. I don’t think we need it. If we let, say, ^x be the capture type of x, then we can just use stuff like (^x & ^y) and live in normal-type-land, not in alternate {}-land.

[odersky]

@Ichoran

It does make me wonder about the whole capture set notation, though. I don’t think we need it. If we let, say, ^x be the capture type of x, then we can just use stuff like (^x & ^y) and live in normal-type-land, not in alternate {}-land.

It’s actually x^ not ^x. And, yes, in 99% of cases this is enough. All our papers so far assume just this. But there are rare cases where we need to specify coupling of capture set variables. That’s what the new syntax is for. We tried to do without for a long time, but in the end there are certain (rare) patterns that are best described that way. A good analogy is with Rust, where usually you don’t need to write explicit lifetimes, but for more advanced patterns you do.

[regiskuckaertz]

@etaconversion

For more extensive usage examples, the CC language reference and the test cases in this PR are a good starting point

hi @etaconversion this is a great read. It seems the feature set and syntax support union of capture sets, in your example

def apply[cap C >: {io} <: {io,network}, cap D <: {C}, cap E >: {C,D}, T, U] ...

I was wondering if you had any plan to support other set operations: difference, negation, intersection? For instance, I’d love to be able to express “here’s a program that accepts any expression that can’t launch the missiles” with first-class syntax, e.g. this strawman:

def program[cap C <: {cap} \ {launchTheMissiles}, A](expr: A^C)

? And if yes, would it make sense to extend the syntax introduced in Scala 3:

• union: A | B
• intersection: A & B
• complement: !A ?
• difference: A \ B ?

As another data point in the design space, Flix also uses set logic for its effect system:

In Flix, the language of effects is based on set formulas:

• The complement of ef is written ~ef.
• The union of ef1 and ef2 is written ef1 + ef2.
• The intersection of ef1 and ef2 is written ef1 & ef2.
• The difference of ef1 and ef2 is written ef1 - ef2.

I was also curious why you made that choice:

A capture annotation ^ binds more strongly than a function arrow.

In the example A ->{c, d} B it gives (A -> B)^{c, d} instead of A -> B ^ {c, d}. Do you foresee that users will more often carry parameters with capabilities rather than functions capturing ones?

[Ichoran]

@odersky

But there are rare cases where we need to specify coupling of capture set variables.

Are there some examples written out somewhere? It’s hard to give feedback on notation when “use existing notation” is out because of some factor that isn’t seen.

In reading through the docs and examples here, it’s hard for me to see any place that actually requires the new notation, which makes it hard to know how to justify using the new notation.

Does it come up with type unions and intersections, for example? That does seem a bit tricky. If A is actually T^C and B is actually U^D then A & B should be (T & U)^{C, D} and A | B should be (T | U)^{C, D} because possibility is enough to require capabilities.

This is an area where my opaque type encoding doesn’t work; I’m not sure whether it’s practical to compute that with match types but my sense is that it certainly isn’t easy. But if the types could be computed, then I think the scheme would still work because {C, D} still maps to (C & D).

@odersky

It’s actually x^ not ^x.

Here is an example of where I think there’s potentially a notational issue.

Conceptually, we have

 /-------- This is the type of what we have
T ^ {C}
   \  \--- This is the type being captured
    \----- This indicates that there is tracking

So if we have a term x then x^ seems like it should mean “the type of x with awareness that it might have captured stuff” while ^x should mean “x viewed as a thing you can capture”.

So if it were possible to use regular type notation instead of capture set notation, you would say something like [cap C >: ^x <: X]. Even though x^ does have to be tracked because it captures something, it’s ^x which naturally is the I-can-capture-you view of things. Put another way, {x} feels like ^x, not like x^.

In general I find that the notation blurs the distinction between tracking, capturing, pure, and anything-goes types too much. While it is true that once you capture something that needs tracking, you yourself also need tracking, for teaching and probably for reading as anything but an accomplished expert, maintaining distinctions is important. implicit implicit and the dozen different meanings of _ come to mind as cases where we wanted to merge things less so that what is going on is clearer.

So it would help, I think, to go exactly the opposite direction of the “we can drop this” suggestions here:

@etaconversion

Consequently, we should have similar expectations for notations compared to higher-kinded type parameters:

def foo[C^, D^ <: C, E <: C]() = ...
//                   ^
//     necessarily a capture variable due to its bound

trait Foo[T <: List[() ->{C} Unit], C^]:
  type D^ <: C
  type E  <: C

That also implies we when we can drop braces (or whatever delimiters) for literal capture sets: when it’s a reference to a single capture-set parameter:

type D^ <: {C}
type D^ <: C

This seems notationally unfortunate. If I care that E has associated capture information, then I should be able to see that whenever it is mentioned. type E <: C essentially loses that information in syntax.

@etaconversion

Here, we have the problem of ambiguity between type- and and term-variable names:

trait Foo[io^]
  val io: Any^
  type C^ <: {io} // ambiguous
  type D^ <: io   // unambiguously the type-level io name

That’s bad style and should result in a warning at the very least.

Here, type D^ <: io isn’t any clearer to me than type D^ <: {io} because I can read either io as the type variable or io.type for the term–you can declare that it’s one way or the other, but just looking (without being told) it is ambiguous either way. It should always be at least a warning, probably an error.

Anyway, it would be nice to be able to fill out a table somewhat like this one with very clear unambiguous entries:

pure type	tracked type	captured type	instance type	any kind of type
pure T	cap T	{T}	T	any T

(Maybe it had better go vertically if there are more concepts that need notation.)

I guess my biggest concerns right now is that many new concepts are being introduced, and (1) I worry that more are being introduced than are really needed even if the ones being introduced are a slightly simpler match to the problem domain, and (2) that the concepts that are being introduced don’t leap out enough because the syntax doesn’t consistently map cleanly and distinguishably onto the concepts.