Questions regarding Capabilities

Language Design
1

I’m working on a comparison between capabilities and algebraic effects. Given that we don’t have much documentation on what capabilities are yet, I’m reaching out to try to clarify some aspects:

1. What are capabilities? It seems Caprese is introducing two different effect trackings: capture tracking (^{...}) and context functions (?=>). Can we say context functions is what is meant as capabilities and capture tracking is a separate solution to make them safe by avoiding escaping? How do these three concepts (capture checking, context functions, and capabilities) relate to each other in Caprese’s design?

2. Do capabilities offer features beyond implicits? I’ve noticed that context functions desugaring generates good bytecode but, other than that, do context functions/capabilities offer any features beyond what can be achieved with regular implicits?

3. How do you combine capabilities? Given that context functions take a single input and that a computation can typically use multiple effects, what’s the recommended way to express an API that requires multiple capabilities? For instance, if a function needs both Async and Database capabilities, is the idiomatic approach (using Async, Database) or is there a composition mechanism like Async & Database? When falling back to regular implicit declaration, is that also considered capabilities?

4. Is there capability inference? Given the nature of implicits/context functions, it seems users will have to manually declare capabilities in method signatures and can’t rely on the compiler’s inference / auto complete to fill them. Is this understanding correct?

5. Will capabilities offer first-class continuations? If I understand correctly, the explorations so far rely on runtime-provided thread blocking, which can be virtual now with Loom. Are there plans to offer more proper support for continuations? How about multi-shot continuations?

6. Are side effecting capabilities purely functional? I’ve been noticing effect tracking via capabilities being mentioned as purely functional. For example, def setState[A](s: A)(using State): Unit = this.state = s requires a State capability but executes a regular side effect immediately. Can that be considered purely functional? If so, what distinguishes this from traditional imperative programming with parameter passing?

7. How do capabilities avoid unsafe compositions? Some capabilities shouldn’t be used in specific contexts. For instance, a State capability being used within parallel computations could lead to inconsistent state. How does Caprese prevent or signal such unsafe usage? If I have a State capability and attempt to use it within Future.traverse or similar parallel constructs, what happens? Is there a way to express that certain capabilities should not be used in specific contexts, or is this left to user discipline?

Thank you in advance,

Flavio

10 Likes
2

Apologies. I forgot an important question.

8. How do I use the latest features?

It seems the development is ongoing in Scala 3’s repository. What is the recommended way or version to play with Capabilities/Caprese?

3

You can read the newly rewritten documentation for capture checking and separation checking here: Scala 3 Nightly Documentation | Capture Checking

  1. capabilities are values - the capability is provided either by the value being in scope if its just a marker, or actual fields/methods on it if there is a real operation. Context function is one way to pass around the value. Capture checking is automatic checking that a capability cant be referenced from some object that leaves the scope where it was defined.

  2. some capabilities are designed to be used with the erased mechanism so have no runtime cost (i.e. only a type-level witness)

  3. capture sets are a new kind of type inferred by the compiler, which contains all the references to captured capabilities - to abstract over multiple capabilities there is a new “capture set” kind of generic type parameter, e.g. [C^]

  4. i think if you are the library author you probably have to manually annotate where the captures are if you want them to be allowed to leak (e.g. that Iterator.map stores the initial iterator and the closure to map with). I think the goal is that for application users they shouldn’t need to do much except enjoy more compile-time safety than with it turned off.

  5. not for me to answer (this question is for core-team)

  6. its low-level imperative programming where you can control what is allowed to occur with static checks, “pure” means no capability allowed to be used. One part however of the separation checking is the ability to “consume” a reference - however i am unsure that you could make e.g. result of println capture some immediately dropped reference?

  7. The idea i believe is that Future would have a closure as a constructor, and that closure would have a type that prevents capturing the state capability - there is a generic mechanism called “capability classifier” which is user pluggable - so you can effectively filter which capabilities should be allowed to come through

  8. see this PR CC Language Reference Improvements v2 by bracevac · Pull Request #23818 · scala/scala3 · GitHub

4 Likes
4

I have the same question about cc. When using Netty’s ByteBuf, which requires us to call release once we finish the usage of Bytebuf, otherwise, if it’s been gc-ed but the reference count > 1, then a leak happens.

So will CC help to check a user forgetting to call release？

I’m reading Nicolas Rinaudo - Hands on Capture Checking

I think there should be more docs and examples of how cc can help users and library authors

5

Thank you for the clarifications! I have some follow ups on the questions if you don’t mind.

  1. Aren’t erased values a different feature? Maybe a better way to formulate it is that capabilities rely on multiple language features like capture checking, erased values, implicits, context functions, etc?

  2. I think this was the most confusing part to me. Reading the documentation, I also saw capabilities always mentioned in the context of the capture sets (^{...}). Are capabilities meant to be tracked via capture sets? My impression was that context functions would be the primary effect tracking mechanism and capture checking is only a way to ensure their soundness.

  3. Do you mean that there wouldn’t be capability tracking in user code? Isn’t the goal to track capabilities like Async or Throw for example?

  4. Why is that? How can we get more info? It’s a major aspect to determine the expressiveness of capabilities.

6

I think the goal is to enable defining APIs that use capture checking to avoid resources escaping a scope, which is something that’s not possible to ensure without capture checking. We’d still need APIs like Resource, Scope, withFile, etc to deal with the actual lifecycle of the resource. Capabilities seem to be modeled only to track effects, not to model their execution given that they lack a runtime component like effect suspension.

7

On the multi-shot continuations - Martin Odersky said at ScalaDays that it would be not a possibility (in the near future) since the target platforms don’t have native support.

i.e. this capability system is designed around making low-level imperative code more safe, so eliminating the need to have an interpreter layer that traditional scala effect sytems add on top

e.g. you could do a thin wrapper over POSIX but add static guarantees about mutability and resource leaks.

in the keynotes it’s always being compared to Rust but as a more flexible system that is intended for a garbage collected language

8

Capabilities are values of types that inherit from caps.Capability. Typically, we don’t use Capability directly, but one of it’s the subtraits, like caps.SharedCapability.

trait Nuke extends caps.SharedCapability
  def launch(): Unit

The focus of capture checking is not directly “this and that effect can happen” like “the nuke could launch”, but instead “these are the resources/objects that are reachable and the allowable effects follow implicitly from those objects’ APIs”. E.g., val nuke: Nuke^ is captured by a function, ergo the function could potentially invoke the methods of nuke, such as launching it.

By marking a type a capability, we signal to the type system that we want those values to be tracked, i.e., how they are retained/closed over by values and computations of other types.

Scala’s (context) function types are not capabilities, but functions (and generally classes/objects) may capture capabilities.
(Though, of course, one could have a capability type with an apply method).
For example val f = () => nuke.launch() would have type () ->{nuke} Unit. The lambda f is not a capability! However, by making use of nuke in its body, we attach the capture set ^{nuke} to f’s type. Tracking captures is contagious: say we eta-expand that function () => f(), then the type of the lambda is () ->{f} Unit, i.e., it captures f, and indirectly nuke. Through subcapturing, we can establish the link {f} <: {nuke}.

Under capture checking, A => B and A ?=> B become shorthands for A ->{cap} B and A ?->{cap} B which in turn are convenience notations for (A -> B)^{cap} and (A ?-> B)^{cap}, i.e., everything is about capturing types of the form T^{c1,...,cn}.
Here, ^{cap} is the special “top” capture set, and that means A => B is a function that “captures arbitrary capabilities”, which is to say it can perform arbitrary effects.

In contrast, A -> B (or equivalently A ->{} B) is a “pure” arrow that captures nothing. The only way in which such a type could perform effects (again showing that capturing is different from traditional static effect systems), is if A was a capability, e.g., (s: State^) => s.write(42) is typeable as State^ ->{} Unit. So if we rule out that A is a thing that can perform effects, then A -> B is indeed a type of pure functions.

IIUC, you are referring to a style that models computations as context functions, and those computations are wrapped in some type constructor indexed by an intersection type of the passed capability types. Computations must be composed by some combinators that do the plumbing.

With capture checking such ceremony should not be necessary as everything is in direct-style Scala. Capabilities are entities bound to variable names, and we predominantly think in terms of capture sets containing variable names. The type system will infer the capture sets and automatically accumulate them in compound expressions.

If we are talking about concrete capability values in the ambient context, e.g., there’s some val async: Async^ and val db: Database^, then just using them in a function’s body will make them appear in the function’s capture set.

Parameterizing over capabilities can be done with function/implicit parameter lists.

Capture sets are inferred by the compiler. Not sure I understand the rest of the question. The system is designed around tracking capture sets, which are sets of variables naming capabilities.

Probably. We are evaluating different approaches. However, this is largely an orthogonal question to tracking capabilities through static typing, and more of a matter of finding/supporting a satisfactory underlying runtime mechanism. With the system’s focus on capabilities and scopes, I’d expect that we’ll end up with lexically delimited continuations similar to those in the Effekt language.

Whether we can offer the full expressive power afforded by general continuations on the JVM is not clear. The question is also whether we truly need their full power and if the price to obtain it is reasonable.

See above. We use the term “pure” if nothing’s captured. Pure in the sense of “free of side effects” requires no captures and not passing any capabilities. However, since the type system is opt-in, it only tracks what we tell it to track. To guarantee absolute purity, it would have to be made mandatory and track everything. Maybe in the distant future we’ll make it mandatory :slight_smile:

We have currently two ways:

  1. Classifier Capabilities enable custom “privilege hierarchies” and we can demand in the types that a function parameter closes over capabilities up to a certain level.
    Example.

  2. Separation Checking when enabled can enforce that threads refer to disjoint sets of capabilities, resp. we can mark a State capability’s state-changing methods as update and only pass a read-only view (preventing callling update methods statically) that is shareable across threads. Separation checking is still fairly new and subject to changes.

9 Likes
9

6. Are side effecting capabilities purely functional? I’ve been noticing effect tracking via capabilities being mentioned as purely functional. For example, def setState[A](s: A)(using State): Unit = this.state = s requires a State capability but executes a regular side effect immediately. Can that be considered purely functional? If so, what distinguishes this from traditional imperative programming with parameter passing?

There’s a lot of confusion in this area because it seems there’s a large difference between how purity is thought about in classic pure fp inspired by haskell, where it means that side effecting operations are suspended inside of a special lazy data structure, usually a lazy monad, and between how caprese uses the term. In Caprese it seems that a function is deemed pure if it doesn’t capture any tracked capability at all.

Consider this:

val add: (Int, Int) -> Int = (a, b) => a + b

This is obviously a pure function - takes two ints, returns an int. Nothing side effecting happening here. Let’s extend this a bit:

//> using scala 3.nightly

import scala.language.experimental.captureChecking
import scala.caps.*

class Console() extends SharedCapability:
  def println(s: String): Unit = System.out.println(s"console: $s")

def log(s: String)(using Console): Unit =
  summon[Console].println(s)

object test:
  val addPure: (Int, Int) -> Int = (a, b) => a + b // same as before

  // this will not compile because the function is no longer pure
  // it now captures the Console capability
  val addWritesToConsole: Console ?-> (Int, Int) -> Int = (a, b) =>
    log(s"adding a ($a) to b ($b)")
    a + b

This kinda makes sense - the function is no longer pure because it does use a side effecting capability. There’s no notion of suspension and deferred execution here - the tracking is static, the execution is strict. My understanding is that once you track mutability and lifetimes like Rust does, there’s little need for suspension because the compiler will stop you from doing something that would cause a problem in runtime (and a bunch of other problems that suspension can’t solve too). It’s a completely different question whether the code will be as easy to refactor as it is with lazy monadic effects and as easy to reason about (once you grok monadic effects, that is) as code that is referentially transparent.

To answer you question about the method requiring State capability in the light of the above information - your setState method is clearly marked as impure by the use of capability. The idea seems to be very up front about side effects that any given piece of code is going to execute instead of deferring them until the end of the world. Moreover, I think this way of implementation of State wouldn’t really have all the benefits of capture checking. To me it seems it should use separation checking which would, I guess here as I’m not yet fluent with CC, require that it’s a consume def setState method. I also guess that it would mean that the encompassing class would have to be extends Mutable and therefore it would be subject to linear typing, ensuring no two aliases can exist at the same time, therefore making mutability safe.

One question to @etaconversion that I have in this context is why this compiles just fine because my understanding says that it shouldn’t:

//> using scala 3.nightly

import scala.language.experimental.captureChecking
import scala.caps.*

class Console() extends SharedCapability:
  def println(s: String): Unit = System.out.println(s"console: $s")

def log(s: String)(using Console): Unit =
  summon[Console].println(s)

object test:
  val addPure: (Int, Int) -> Int = (a, b) => a + b // same as before
  
  given Console = Console() // provide capability locally
  
  // and this is now considered pure somehow 
  val addWritesToConsole: (Int, Int) -> Int = (a, b) =>
    log(s"adding a ($a) to b ($b)")
    a + b
10

It should not and it’s a bug. If you turn test into a def, it will exhibit the correct behavior and reject addWritesToConsole. We’re fixing it.

4 Likes