Capture Checking Notes

Capture checking is an experimental Scala 3 type-system feature that tracks which capabilities - open files, connections or other resources, a value’s type has closed over.

In other words, capture checking lets the compiler track which resources a piece of code depends on, so it can catch at compile time if that code tries to use a resource after it’s been closed/released.

Capture checking is achieved via capturing types in the following form:

T^{c1, ..., cn}

T is the capturing type
{c1,...,cn} is the capture set, where c1,…cn are references to Capabilities.

Capability

Capability is a method or class parameter, local variable, or this of the enclosing class.
Capabilities are tracked. This means the type definition captures the capabilities that can be accessed by values of that type. For example, A^{c} is the type of values of type A that can access the capability c.
The type of a capability is the capturing type with a non-empty capture set.

Capabilities are passed down or derived from the universal capability, which is written as T^{any} or T^ for shorthand.
T^ means it can capture arbitrary capabilities.
T^{} means it cannot capture any capabilities.

Motivating Example from the documentation

def usingLogFile[T](op: FileOutputStream => T): T =
  val logFile = FileOutputStream("logs.txt")
  val result = op(logFile)
  logFile.close()
  result

usingLogFile(fs => fs.write("hello))

Abuse …

val later = usingLogFile(fs => () => fs.write("BOOM!"))
...
later() //  IOException! later() uses `fs` long after it is closed

How to avoid abuse

Enter capture checking …

def usingLogFile[T](op: FileOutputStream^ => T): T =
  val logFile = FileOutputStream("logs.txt")
  val result = op(logFile)
  logFile.close()
  result

Note the FileOutputStream^. That turns the parameter ( logFile ) into a capability whose lifetime is tracked.

val later = usingLogFile { f => () => f.write("hello") }
                                ^^^^^^^^^^^^^^^^^^^^^^^^
The expression's type () => Unit is not allowed to capture the root capability `any`. 
This usually means that a capability persists longer than its allowed lifetime.

Terminology

class Logger(file: File)

val out: File^ = new File("/path/to/file")
val lg: Logger^{out} = new Logger(out)

lg is of type Logger and can access out. Or we say lg captures out.
Logger^{out} is a capturing type.

def mkLogger(out: FileOutputStream^): Logger^{out} =
	new Logger:
		def log(msg: String) = out.write(msg.getBytes)

This is okay

val xs = usingLogFile { f =>
  List(1, 2, 3)
    .map { x => 
      f.write(x)
      x * x 
    }
}

But using a LazyList makes it unsafe, and so will encounter a compilation error! The standard library has been annotated with ^s already for us.

A generic try-with-resources like function

def using[R <: AutoCloseable, T](resource: R^)(op: R^{resource} => T): T =
  try op(resource)
  finally resource.close()

val result = using(FileOutputStream("log.txt")) { r =>
  r.write("hello")
  42
}

Capture Checking in Functions

A -> B
// Pure function that does not capture any capabilities
// Equivalent to (A -> B)^{} or A ->{} B

A => B
// Impure function that may capture any capability
// Equivalent to (A -> B)^{any} or A ->{any} B

(A -> B)^{x, y}
// Impure function that captures _only_ `x` and `y` capabilities.

Purity

“purity” here is entirely about the presence of a capture set, not about side effects.

A type with no capture set is pure. A or A^{}

A type with a capture set is impure. A^ or A^{any}, A^{x, y}.

Some more example(s) … just for reinforcement

class Logger(fs: PrintStream^):	// capturing class with a tracked capability
  def log(s: String): Unit = ...

val l: Logger^{fs} = Logger(fs) // NOT pure — capturing type, tied to fs
(A -> B)^{x, y}                 // NOT pure, has a capture set

val n: Int        = 42			// pure — Int carries no capability
val s: String     = "audit"		// pure — String carries no capability
val f: Int -> Int = x => x + 1	// pure function — captures nothing

Recap

A is the same as A^{}. Pure, does not capture anything.
A^ is the same as A^{any}. Impure. Captures the root capability.
A -> B is the same as (A -> B){}. Pure, does not capture anything.
A => B is the same as (A -> B){any}. Not pure, may capture anything.

Notation	Capture set	Pure type?	Equivalent to
`A -> B`	`{}`	Yes	`(A -> B){}`
`A ->{x,y} B`	`{x,y}`	No (capturing, but bounded)	—
`A ->{any} B`	`{any}`	No (capturing, unbounded)	`A => B`
`A => B`	`{any}`	No	`A ->{any} B`
`(A => B){...}`	n/a	n/a	not valid/meaningful — `=>` isn’t re-annotatable

Subtyping and Subcapturing

T₁ <: T₂ // ordinary subtyping

C₁ <: C₂ // means capture set C₁ is covered by C₂

T^C1 <: U^C2 // if T <: U and C1 <: C2

Capturing influences subtyping

Subcapturing – Subtyping with capture sets

Rule of thumb: A smaller capture set gives a subtype.

A value that captures less can be used where one that captures more is expected.

👉 progressively wider capture sets, each one a super type of the last

A <: A^{out} <: A^{out, f} <: A^{lg, out, f} <: A^ // general rule

A pure type is a subtype of any capturing version of itself.

T <: T^C

A <: A^{lg} <: A^{out} <: A^{out, f} <: A^ // Per the logger example(s)

Step	Reduced obligation	Justification
`A <: A^{lg}`	`{} <: {lg}`	purity / empty set is covered by anything
`A^{lg} <: A^{out}`	`{lg} <: {out}`	logger-specific: `lg : Logger^{out}`, so `lg` refines {out}
`A^{out} <: A^{out, f}`	`{out} <: {out, f}`	`out ∈ {out, f}`
`A^{out, f} <: A^`	`{out, f} <: {any}`	`A^ = A^{any}`, and `{any}` covers everything

lg itself has type Logger^{out}, lg’s own capture set is {out}.
Rule: if c has capturing type A^{c₁,...,cₙ}, then {c} <: {c₁,...,cₙ}.
So {lg} <: {out}, meaning anything that can only capture lg can equally be treated as capturing out (since lg is “made of” out — you can’t get more authority through lg than out already grants). This is the “derived from” relationship from a few turns back: lg’s authority traces back to out, so {lg} is narrower/more specific than {out}.

class Tracked(override val toString: String = "Tracked")

class Indirect(val t: Tracked^) extends Tracked(s"Indirect($t)")

class SubButNot extends Tracked(s"SubButNot")

case class Tracker(val t: Tracked^)

@main def run(): Unit =
  val t: Tracked^ = new Tracked

  val sd           = new Tracker(t)					// Base
  val si           = new Tracker(new Indirect(t))   // Subclass and subcapture
  val sn: Tracker^ = new Tracker(new SubButNot)		// Subclass but not subcapture

  def foo(f: Tracker^{t} => Unit): Unit =
    f(sd)
    f(si)
    // f(sn)

  foo(f = a => println(s"$a"))

import language.experimental.captureChecking

trait Logger:
  def log(msg: String): Unit

// 1. Uses only fs  -> captures {fs}
class FileLogger(fs: FileOutputStream^) extends Logger:
  def log(msg: String): Unit = fs.write("app.log", msg)

// 2. Uses fs and ct -> captures {fs, ct}
class StrictLogger(fs: FileOutputStream^, ct: CanThrow[Exception]^) extends Logger:
  def log(msg: String): Unit =
    if msg.isEmpty then throw new Exception("empty message")  // uses ct
    fs.write("app.log", msg)

// 3. Uses nothing -> pure
object NullLogger extends Logger:
  def log(msg: String): Unit = ()

def runWith(logger: Logger^{fs, ct}): Unit =
  logger.log("starting")
  logger.log("done")

def runner(fs: FileOutputStream^, ct: CanThrow[Exception]^): Unit =
  val file   = FileLogger(fs)          // type: FileLogger^{fs}
  val strict = StrictLogger(fs, ct)    // type: StrictLogger^{fs, ct}

  runWith(file)        // OK: {fs} <: {fs, ct}
  runWith(strict)      // OK: {fs, ct} <: {fs, ct}
  runWith(NullLogger)  // OK: pure <: anything

Other Areas/Applications (not covered today)

Separation Checking
Capability Tunneling
Extension Methods
Path-dependent Types and Type parameters
Checked Exceptions

Capture Checking tracks which capabilities a value retains; separation checking additionally ensures that capabilities which allow mutation are uniquely referenced, preventing aliasing surprises.