About Capture Verification

scala 3

A few days ago we saw a new experimental feature called “capture check” (capture checking), announced in tweet Martin Odersky.

This feature is the new chapter in a decade-long struggle to add some form of effects system to scala 3. It bears some resemblance to the proposal linear constraints (linear constraints) for Haskell and at times of life (lifetimes) Rust.

Disclaimer:

all code snippets shown here are not guaranteed to be type-matched and should be treated as scala-like pseudo-languages

Effect systems

An effects system is something like meta-information, usually inside a type system. It checks and warns that the runtime value or other semantics of the current expression has some peculiarities, such as side effects, asynchrony, errors, indeterminism, multiplicity, and the like.

A complete algebraic effects system needs several components:

• A composition that combines all the effects on the go.

• A type system comparable in behavior to semilattices.

• An effect processing that embodies the cut rule in its logic.

The first one means that if we write something like foo(bar(x)) or foo(x) + bar(y), where foo has effect Abut bar has effect B, then the entire set of this operation must have the effect “A + B“, where “A” And “B” can be anything from changing some variables to parallel inter-node communication.

The second one means that you have some kind of effect “adding” operation, commutative and idempotent. I.e a + b + a, a + b And b + a the result is the same.

The third one means that sometimes you can take some expression with compound effect likea + band as soon as some “handler” becomes available for you to byou can apply it to your expression and get some new expression only from mark a On him.

Scala 3 had several possible mechanisms to provide such a system, these two being notable:

Both offer effects as possibilities, i.e. requiring an object of some type is an effect, and providing a required object is processing.

The first is based on the fact that scala 3 already has a nice subtype lattice. This means that, having some contravariant type Expr[-_]you can get a rule when composing expressions with Expr[A] And Expr[B] lead you to some Expr[A & B] with all commutativity and idempotency for free. The first version of the ZIO module template relied heavily on this.

However, the “handling” was problematic, as it is not easy to write a correct runtime that can “subtract” one trait from another, which would eventually lead you to need to “merge” traits, i.e. provide a common function that performs (A , В) => А & В.

This was first partially solved by the macros in the “zio-macros” library.

Then there was a partial solution based on HashMap from TypeTag-keys called Has in ZIO. And ZIO-2 is going to make that hashmap completely hidden, leaving the user with types like Console & ReadUser & Postgreswhere everything Console, ReadUser And Postres are naked traits, not aliases Has.

The second option, contextual abstraction, was of particular interest to Martin Oderski. He felt that the mechanism for implicitly passing arguments at cast time was the best form of a possibilistic effects system. So have effects A And B as simple as having contextual type arguments A And Bi.e. have the type (A, B) ?=> Whatever.

This mechanism has simple effect handling – it’s just passing an argument. However, this requires a lot of effort from the user in typing, since the contextual arguments can’t be inferred yet.

It also lacks basic properties such as (A, B) ?=> X not the same type as (B, A) ?=> X . And what’s worse when B is a subtype Aso A ?=> X is a subtype B ?=> X for anyone Xthen it is not true that (A, B) ?=> X coincides with B ?=> X

But these were not the problems that Martin was worried about. The most significant problem for him was the problem of “opportunity leakage”. So imagine that you have Database ?=> User. Technically you can provide some Database and now have a clean value Userbut there is no guarantee that some method or function inside User did not capture this Database. And you continue your calculations, now formally, regardless of Databasebut somewhere all of a sudden you initialize a SQL transaction using an old and possibly closed database session.

Command dotty was so obsessed with this problem that she rewrote one of the most exciting things about the type system rust: lifetime.

Lifetime

Imagine that you have a compiler that builds an application without garbage collection support and copies as little data as possible. So when you allocate something on the heap or stack, you need to encourage reuse of that data by using some bare object references not tracked by the garbage collector.

Here is rust and introduced the parameters of the lifetime (lifetime).

Each function or type can have common parameters such as 'a 'bthey can optionally be applied to some link or other shared object and have the meaning of “lower bound on how long this link will live” or “interval in which this link is guaranteed to be valid”.

Thus, the following pair of definitions has completely different semantics:

fn get_something<'a>(src: &'a Source) -> Something

fn make_something<'a>(src: &'a Source) -> Something<'a>

If the return type doesn’t mention the lifetime of the parameter, the function is probably doing something, accessing the arguments while it’s doing it, and generating a result completely independent of the argument.

The second means that the function probably takes an argument and puts a result into it, so the result type is likely to be incorrect when the original referenced value is moved or removed.

Capture check

The dotty command offers something similar in scala 3. But instead of additional ephemeral types, it presents lifetimes with the names of the corresponding parameters. The first option would look traditional.

def getSomething(using src: Source): Something

And in the second, now there is an elegant mark on the type

def makeSomething(using src: Source): {src} Something

So, instead of adding special named type labels, we can just use the argument names as their “lifetime”.

So why is this even relevant in a runtime language with garbage collector support like scala?

First, and most obviously, it solves the problem of “leaking opportunities”. Now whenever Database has the trait @capabilityyou cannot write Database ?=> User unless the result is a value unrelated to database. Instead it should be something like

capture dependent function.scala

(db: Database) ?=> {db} User // синтаксис не утвержден

So you have to explicitly state somewhere that the result type is not free from db. Does this make contextual abstractions a good effects system? It’s hard to answer this question, but I think it gives us a much more interesting thing.

It should be noted that capture checking does not include “linearity” or any other form of substructural typing. If we check carefully, none of the three most common structural rules (weakening, contraction, exchange) will be violated. The most complex of these, “reducing” which allows for “reusability”, is still safe. Although final types can refer explicitly to context variable names, so does the dependent type system, and the logic involved is not substructural. We can simply “reassign” multiple names to a single variable during compression.

Resource scopes

A typical parallel application that takes resources into account in Cats-effect or ZIO uses a monadic type resource or ZManaged. This type is usually based on some basic asynchronous monad, say F[_] or ZIO and includes:

So a typical use of this type would be resource.use(actions)which is roughly equivalent to

for
  (r, release) <- resource.allocate
  x <- actions(r)
  _ <- release
yield x

Your resource can be composite, you can have multiple resource allocation routines, and something like:

val resource = 
  for 
    a <- resA
    b <- resB(a)
    c <- resC(a, b)) 
  yield f(a, b, c)

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

for
  (a, releaseA) <- resA.allocate
  (b, releaseB) <- resB(a).allocate
  (c, releaseC) <- resC(a, b).allocate
  x <- actions(f(a, b, c))
  _ <- releaseC
  _ <- releaseB
  _ <- releaseA
yield x

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

What if we need something like:

for
  (a, releaseA) <- resA.allocate
  (b, releaseB) <- resB(a).allocate
  x <- f(a, b)
  (c, releaseC) <- resC(a, b, c).allocate
  _ <- releaseA
  y <- g(b, c)
  _ <- releaseB
  _ <- releaseC
yield h(x, y)

In this code, we assume that resB And resC use resA during initialization, but do not need it during its existence, so any function g can refer to them without fear. But there is a feeling that such flows are hard to express using the current form of a statically scoped resource.

RAII

One of the nicest things about rust’s lifetime is that it helps you manage resources efficiently.

The above code can be converted to something like

let a = res_a()
let b = res_b(&a)
let x = f(&a, &b)
drop(a) // optional
let c = res_c(&a, &b)
let y = g(&b, &c)

The first thing we can see here is that there is no need for deallocators, not even drop(a) optional, as rust can automatically calculate the reset time for each variable.

Second: although a discarded, we can freely use b And c since their lifetime is presumably not tied to a.

Third, we don’t have a “resource” type here. Each construct can serve as an allocation of resources.

Unfortunately, these subtleties are difficult to use in parallel code. The most popular implementations of asynchrony in Rust use a global loop to schedule tasks. Every Task is a special case Future and must have ‘static lifetime so that it can be scheduled. This means that variables allocated in one task cannot be used as “watch-for-life” resources in another. Therefore, if your “resource” is to be used competitively, it is difficult to keep track of its “lifetime”.

Capture and RAII verification

Something similar could be achieved in the new proposal. You can distinguish between three types of usage, for example,

def useA(a: A): {a} IO[B]

def useA(a: A): IO[{a} B]

def useA(a: A): {a} IO[{a} B]

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

It also means that we can technically have something like a resource without having to use different monadic types. However, we must add some note about natural “resources”, things that need to be released.

Let’s say the standard calculation would be of type IO[normal, A] and resource-like IO[resource, A]. We must adapt our flatMapi.e.

//ordinary calculation
extension [A] (io: IO[normal, A)
    def flatMap[flag, B](f: (a: A) -> {a} IO[flag, {a} B]) : IO[flag, B]

//resource allocation
extension [A](io: IO[resource, A])
// using the resource
  def flatMap[flag, B](f: (a: A) -> {a} IO[flag, B]): IO[flag, B]
// defering the deallocation
  def flatMap[B](f: (a: A) -> {a} IO[Any, {a} B]): IO[resource, B]

This also means that we need a more complex for comparison (or other syntactic sugar) that can complete flatMap before the whole expression stops, so:

for
  a <- resA
  b <- resB(a)
  c <- resC(a, b)
  x <- foo(b, c)
yield bar(x)

can be converted to

resA
  .flatMap(a =>
    resB(a)
      .flatMap(b =>
        resC(a, b)  
          .map(c => (b, c))
  )
  .flatMap((b, c) => 
    foo(b, c)
      .map(bar))

Notice the left associated flatMap on the resA to pre-close a resource based on the fact that b And c don’t fix the link a.

We can also add (a)to ensure proper termination of life.

These flags `normal` and `resource` can most likely be thrown out with some additional “capture” annotation, since (r: Release) ?-> {r} Async[A] can be an alias for IO[normal, A] as well as (r: Release) ?-> {r} Async[ {r} A] will be an alias for IO[ресурс, A]– a computation that requires completion of work.

Thus, instead of having a specific monad for resources, we can have a scope label representing operations on the scope.

Final Thoughts

Resource allocation is just one example of how the new capture check mechanic can be used.

But the story doesn’t end there. In short, I don’t think the capture test ends with effect tracking. I find this to be a great tool for keeping track of scopes.

There are many more parallel scoping issues such as

• Competitive blocking.

• Database sessions.

• Custom HTTP sessions.

• STM.

Every time we have some sort of monadic helper type translated into IO, we introduce a special scope, and scope interaction becomes complicated.

Capture checking adds the ability to have area intersections and replaces each highly specialized type of area marking with a single lexical “opportunity”.

This allows scope traversal and possibly eliminates functor zoos in existing parallel libraries.

---

Soon OTUS will host an open lesson “Functional Design in Scala”, to which we invite everyone interested. In this lesson we:
— let’s talk about 2 approaches in functional design;
– consider the main components, features;
Let’s solve the problem using each of them.
registration link.