by Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, and Aleksander Boruch-Gruszecki

In Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2022.

This publication is related to the Lexical Effect Handlers research project.

This publication is related to the Type- and Effect Systems research project.

Abstract

Reasoning about the use of external resources is an important aspect of many practical applications. Effect systems enable tracking such information in types, but at the cost of complicating signatures of common functions. Capabilities coupled with escape analysis offer safety and natural signatures, but are often overly coarse grained and restrictive. We present System C, which builds on and generalizes ideas from type-based escape analysis and demonstrates that capabilities and effects can be reconciled harmoniously. By assuming that all functions are second class, we can admit natural signatures for many common programs. By introducing a notion of boxed values, we can lift the restrictions of second-class values at the cost of needing to track degree-of-impurity information in types. The system we present is expressive enough to support effect handlers in full capacity. We practically evaluate System C in an implementation and prove its soundness.

Interactive Example Program

The following example program illustrates how System C tracks capabilities.

interface Console { def println(msg: String): Unit }

Function helloWorld takes a capability to write to the console. The inner function nested simply closes over the capability – its type is () -> Unit. However, the type system keeps track of the fact that it closes over console (try clicking typecheck and edit to interact with the type checker).

def helloWorld { console: Console }: Unit {
  console.println("hello");
  def nested(): Unit { console.println("world") }
  nested()
}

There are many more examples and much more explanation in the artifact that accompanies the paper.

Paper Website with More Examples

News

Related Publications