About capture checking

in scala 3

Several days ago, we saw the new experimental feature called “capture checking” was announced in the tweet by M. Odersky.

This feature is a new chapter in a decade-long struggle for adding something like an effect system to scala 3. It has some similarities with the linear constraints proposal for Haskell and rust lifetimes.

Disclaimer:

all of the code snippets here are not type-checked and should be considered scala-like pseudo-language

Effect systems

Effect system is some form of metainformation, usually inside the type system. It alerts and checks that the runtime meaning or other semantics of the current expression has some special things, such as side effects, asynchronicity, errors, indeterminism, multiplicity, and whatnot.

A full-blown algebraic effect system needs several components:

• A composition that aggregates all the effects on the go
• A type system that behaves something like a semilattice
• An effect handling that looks something like a "Cut" rule in logic

The first one means that if we write something like foo(bar(x)) or foo(x) + bar(y) where foo has effect A and bar has effect B, that whole operation should have an 'A + B' effect. Where 'A' and 'B' can be anything from mutating some variables to parallel internode communication

A Second one means that you have some "adding" effects operation, commutative and idempotent. That is a + b + a, a + b, and b + a are all the same thing.

A third one means that you can sometimes take some expression with a complex effect like a + b and as soon as you have some "handler" for b you can apply that handler to your expression and get some new expression with only a mark on it.

Scala 3 had several possible mechanisms providing for such a system, notable two are:

• Contravariance
• contextual abstraction

Both are suggesting effects as capabilities. I.e., requiring an object of some type is the mark of effect, and providing a required object is handling.

The first one is based on the fact scala 3 already has a nice subtyping lattice. Meaning having some contravariant type Expr[-_] you can end up with the rule when composing expressions with Expr[A] and Expr[B] will lead you to some Expr[A & B] with all the commutativity and idempotence for free. That was fully exploited by the first version of the ZIO module pattern.

However, "handling" was troublesome since it's not that easy to write a correct runtime that can "subtract" one trait from another, which eventually would lead you to the need of "merging" traits, i.e., providing a general function doing (A, B) => A & B.

That was partially solved first by macros in the "zio-macros" library.

Then, a partial solution based on a TypeTag-keyed HashMap called Has arrived at ZIO. And ZIO-2 is going to make this hashmap completely hidden, leaving a user with types like Console & ReadUser & Postgres, where all of the Console, ReadUser, and Postres types are bare traits and not aliases to Has.

The second option, a contextual abstraction, was particularly interesting to M.Odersky. He felt that the mechanism of implicitly passing arguments during application is the best form of a capability-type of effect system. So having effects of A and B is easy as having contextual arguments of types A and B, i.e., having type (A, B) ?=> Whatever.

This mechanism has a straightforward effect handling - it's just an argument passing. However, it requires more direct typing effort from the user since contextual arguments can't be inferred yet.

Also it lacks basic properties since (A, B) ?=> X is not the same type as (B, A) ?=> X . And what is worse when B is a subtype of A, so A ?=> X is a subtype of B ?=> X for any X it's not true that (A, B) ?=> X is the same as B ?=> X

But those weren't the issues that Martin was sad about. The most considerable trouble for him was a "capability leaking" problem. So imagine you have Database ?=> User. Technically you can provide some Database and now have a pure value of User, but there is no guarantee that some method or function inside the User hasn't captured this Database instance. So you continue your calculation, now free of Database formally and somewhere you start an SQL transaction all of sudden, using an old and maybe closed database session.

The dotty team was so obsessed with this misfortune that it reimplemented one of the most exciting things in rust type system: lifetimes.

Lifetimes

Imagine you have the compiler that builds an application with no garbage collection support and as small copying data as possible. So when you allocate something on the heap or the stack, you need to encourage to reuse this data, using some GC-untracked bare references to the object.

So rust introduced lifetime parameters.

Every function or type can have generic parameters like 'a 'b, these can be further applied to some reference or another generic entity and have meaning "lower bound of how long this reference will leave" or "an interval where this reference is guaranteed to be correct."

So the following couple of definitions have drastically different semantics

If the return type doesn't mention the parameter's lifetime, the function probably performs something, access arguments during it, and constructs the result, totally independent of the argument.

The second means that the function probably uses the argument and puts it the result, so the result type will most likely be incorrect when the initially referenced value is moved or dropped.

Capture checking

The dotty team offers something similar in scala 3. But instead of presenting additional ephemerous types, it represents lifetimes with names of corresponding parameters. The first variant would look traditionally.

And second, now have some exquisite mark on the type

So instead of adding the special named type marks, we can just use argument names as their "lifetimes".

So why is this even relevant to a language with GC-enabled runtime such as scala?

First and most obvious, it solves the "leaky capability" problem. Now whenever Database is a trait marked with the @capability annotation, you can't write Database ?=> User function unless the result is a Database-irrelevant value. Instead It should be something like

So you must somewhere explicitly mark that a result type isn't free of db. Does this enable contextual abstractions as a good effect system? It's hard to answer this, but I think it does a much more interesting thing.

One should be aware that capture checking does not involve "linearity" or another form of substructural typing. If we check carefully, none of the three most common structural rules (weakening, contraction, exchange) is compromised. The most tricky one, "contraction," which provides "reuse" ability, is still safe. Although conclusion types can explicitly refer to a context variable's names, so does the dependent type system, and corresponding logic is not substructural. We can just "reassign" several names to a single variable during contraction.

Resource scopes

A typical resource-aware concurrent application in cats-effect or ZIO uses Resource or ZManaged monadic type. This type is usually based on some underlying asynchronous monad, say F[_], or ZIO, and includes:

• a step to initialize resource
• a step to release the resource.

So typical usage of such type would be resource.use(actions), which is roughly equivalent to

You resource can be compound, you can have several resource allocating procedures and have something like

When you write something like resource.use(actions) whole sequence will look like

Resources have something like a statically known lifetime. Resource c lives from line 4 to 6, b lives from 3 to 7, and a from 2 to 8.

What if we need something like

In this code, we assume that resB and resC only use the resA result during initialization but don't need this during its life so that any function g can reference them without fear. But it seems that flows like that are difficult to express using the current form of static-scoped resource.

RAII

One of the nicest things about lifetimes in rust is that it helps to deal with the resources efficiently.

A code above can be translated to something like

The first thing we can see here - there is no actual need for deallocators, even drop(a) is optional since rust can automatically calculate drop time for each variable.

The second one: although a is dropped, we can freely use b and c since their lifetimes are supposedly not bound to a's.

The third is that we don't have a "resource" type here. Every construction can serve as a resource allocation.

Unfortunately, these niceties are hard to use in the concurrent code. Most popular rust implementations of asynchronicity use a global loop to schedule tasks. Each Task element is a special case of Future and must have a 'static lifetime to be scheduled. That means variables allocated in one task can’t be used as “lifetime tracked” resources in another. So if your "resource" should be used concurrently, it is tough to track its "lifetime."

Capture Checking And RAII

In the new proposal, one can achieve something similar. You can distinguish between three types of usage, such as

The capture annotation before the IO means you can refer {a} during the calculation process. On the other hand, the annotation before B types reflects that the calculation result will still refer to the argument somehow.

That also means that technically we can have something like a resource without the need for different monadic types. Yet we must add some kind of mark on natural "resources", things that need deallocation.

Say the standard calculation will have the type IO[normal, A] and resource-like IO[resource, A], we should adapt our flatMap accordingly. I.e.

That also means we need some more sophisticated for-comprehension (or other sugar) that could terminate flatMaps before the whole expression stops, so that:

could be translated to

Note the left-associated flatMap on resA to close the resource preliminary based on the fact that b and c are not capturing a reference.

We can also add drop(a) here to enforce the correct end of life.

These `normal` and `resource` flags most probably can be thrown out using some additional "capture" annotation such as (r: Release) ?-> {r} Async[A] can be an alias for IO[normal, A] and (r: Release) ?-> {r} Async[ {r} A] will be an alias for IO[resource, A]- a calculation that need some closing job.

So instead of having a particular monad for resources, we can have a scope mark representing scoped operations.

Final thoughts

Resource allocation is just one of the examples of how one can use the new capture checking mechanics.

But it's not the end of the story. In short - I don't think that capture checking is about effect tracking. I believe it's a beautiful tool for scope tracking.

There are much more scope-enabled concurrent problems such as

• Concurrent Locks
• Database sessions
• User HTTP sessions
• STM

Every time we have some auxiliary monadic type translated to IO, we introduce a special scoping, and scopes' interoperations are tricky.

Capture checking adds an ability to have scope intersections and replace every narrow-purpose scope-marking type with a single lexical "capability."

It enables the "intersection" of scopes and possibly eliminates functor zoos in existing concurrent libraries.