Select Page

PL Perspectives

Perspectives on computing and technology from and for those with an interest in programming languages.

Soundly Handling Linearity

by Wenhao Tang, Daniel Hillerström, Sam Lindley, and J. Garrett Morris on Aug 12, 2024 | Tags: , , ,

Soundly Handling Linearity

Picture by Xueying Qin

Programming languages can statically ensure that certain resources are used exactly once through a linear type system based on Girard’s linear logic. Typical linear type systems track the number of times that variables are used under the assumption that continuations are always used linearly. Alas, this assumption is false in programming languages with powerful non-linear control flow features. For instance, in POSIX C the process duplication function fork() returns to its caller twice. More generally control operators such as Plotkin and Pretnar’s effect handlers, as in the web-programming language Links, enable the programmer to capture a continuation and then invoke it more than once or drop it altogether.

Soundly handling linearity requires special care in the presence of effect handlers, as the programmer may inadvertently compromise the integrity of a linear resource. For instance, duplicating a continuation that closes over a resource can lead to the internal state of the resource being corrupted or discarding the continuation can lead to resource leakage. Thus a naïve combination of linear resources and effect handlers yields an unsound system.

We illustrate the issues that arise with combining linearity with effect handlers by way of a soundness bug in the programming language Links, which supports both effect handlers and linear session types. We will use a session-typed channel as our linear resource. Consider a scenario involving a grocer, who sells fruits, and an indecisive buyer, who wishes to buy six apples or six bananas.

The kinds of fruit provided by the grocer are apples and bananas.

typename Fruit = [|Apple | Banana|];

For convenience, we define helper functions for printing a kind of fruit as a string and for the price the grocer charges for each kind of fruit.

fun fruitToString(f) {
  switch (f) {
    case Apple -> "apple"
    case Banana -> "banana"
  }
}

fun fruitPrice(f) {
  switch (f) {
    case Apple -> 100
    case Banana -> 20
  }
}

The grocer and buyer communicate over a session-typed communication channel. The channel has two endpoints: one for the grocer and one for the buyer. We write the protocol for the grocer’s endpoint as the session type ?Fruit.!Int.?Int.End. This session type specifies that the grocer receives a kind of fruit (?Fruit), sends the price of the fruit (!Int), receives a quantity (?Int), and then ends the communication (End). (Of course, the protocol captures only the communication of data, not the actual money or fruit.) Dually, we write the protocol for the buyer’s endpoint as the session type !Fruit.?Int.!Int.End. This session type specifies that the buyer sends a kind of fruit, receives its price, sends a quantity, and then ends the communication.

We model the grocer as a function that initiates the purchase protocol by opening the session-typed channel and returning the buyer’s endpoint.

sig grocer : () ~> !Fruit.?Int.!Int.End
fun grocer() {
  fork(fun(c) {
    var (f, c) = receive(c);                             # receive the kind of fruit
    var c = send(fruitPrice(f), c);                      # send the price
    var (i, c) = receive(c);                             # receive the quantity
    println(intToString(i) ^^ " " ^^ fruitToString(f));  # convert, concat, and print
    close(c)
  })
}

The function fork creates a child process and two endpoints of a session-typed channel. The child process runs the argument function. One endpoint is passed to the child process and the other is returned to the caller. Here, fork returns an endpoint of type !Fruit.?Int.!Int.End (for the buyer) and the child (grocer) process is supplied with the dual endpoint c of type ?Fruit.!Int.?Int.End. The grocer receives a kind of fruit, sends the corresponding price, receives the quantity, prints the kind of fruit and quantity before closing the endpoint.

Now we invoke grocer in the context of an indecisive buyer (the parent process acts as the buyer), where we model the indecisiveness using a variation of the nondeterminism effect: we use the ability to invoke a captured continuation multiple times as well as the ability to drop a captured continuation. The idea is to exploit the non-linearity of continuations in the implementation of nondeterminism to violate the protocol by corrupting the internal state of the channel by sending two kinds of fruit (rather than a kind of fruit followed by an integer) along the endpoint returned by the grocer.

# to enable effect handlers in Links use the command-line flag --enable-handlers
handle({
  var c = grocer();                           # contact the grocer
  var f = if (do Choose) Apple else Banana;   # choose a kind of fruit
  var c = send(f, c);                         # send the kind of fruit to ask for its price
  var (p, c) = receive(c);                    # receive the price
  if (p > 42) throw()                         # give up if the price is too high
  else ();                                    # continue if the price is right
  var c = send(6, c);                         # ask for 6x the chosen fruit
  close(c)
}) {
  case <Throw>             ->  ()
  case <Choose => resume>  ->  resume(true); resume(false)
}

The auxiliary throw function allows us to perform the Throw operation in a context expecting a value of any type at all. This is possible exactly because the return type of Throw is the uninhabited type Zero, which means that it can never actually return a value, and so must behave like an exception.

sig throw : () { Throw : () => Zero | e }~> a
fun throw() { switch (do Throw) { } }

We install an effect handler which handles two operations:

  1. Choose : () => Bool, which returns twice, behaving as a nondeterministic choice.
  2. Throw : () => Zero, which does not return at all, behaving as an exception.

The handled computation invokes grocer, forking the grocer process and binding the output endpoint of the resulting channel to c. The remainder of this computation models the buyer. It first invokes the operation Choose in order to decide whether to buy apples or bananas. After receiving its price, it performs the Throw operation if the price is too high, modelling the fact that the price is too high so the buyer decides to leave. Finally, the computation sends the integer 6 as the quantity along the channel and closing it.

This is all very well and satisfies the type-checker. However, the described control flow is not actually what happens when the price of apples is higher than 42, because in fact the continuation of Choose is invoked twice and the continuation of Throw is never invoked.

The behaviours of Throw and Choose are defined by the corresponding operation clauses of the handler. For Throw the captured continuation is discarded (it is never bound); for Choose the continuation is bound to resume and invoked twice: once with true and then again with false.

Running the program causes a runtime crash when printing the received values in the grocer function, as it erroneously interprets a kind of fruit as an integer in the intToString conversion procedure. To see why, let us follow the control flow of the buyer process. It performs Choose, which initially selects Apple and sends it over the channel.

The grocer process receives the kind of fruit and subsequently sends its price. The grocer process then expects to receive an integer. Meanwhile on the buyer process, execution is aborted via Throw because the buyer decides that apples are too expensive, which causes the initial invocation of resume to return, leading to the second invocation of resume, which restores the aborted context at the point of selecting a kind of fruit. Now Choose selects Banana and sends it over the channel. The grocer process receives this second kind of fruit, mistakenly treating it as an integer!

In the remainder of this blog post we describe a novel approach to rule out such soundness bugs by tracking control-flow linearity, a means to statically assure how often a continuation may be invoked which mediates between linear resources and effectful operations in order to ensure that effect handlers cannot violate linearity constraints on resources. We focus on our implementation in Links. The full technical details are available in our open access POPL’24 distinguished paper Soundly Handling Linearity.

Effect Handlers Break Linearity

Let us take a look at the type and effect signature of the buyer code. We pull out the code into a function in order to give it its own signature.

sig buyer : (!Fruit.?Int.!Int.End) { Choose: () => Bool, Throw: () => Zero | e }~> ()
fun buyer(c) {
  var f = if (do Choose) Apple else Banana;   # choose a kind of fruit
  var c = send(f, c);                         # send the kind of fruit to ask for its price
  var (p, c) = receive(c);                    # receive the price
  if (p > 42) throw()                         # give up if the price is too high
  else ();                                    # continue if the price is right
  var c = send(6, c);                         # ask for 6x the chosen fruit
  close(c)
}

Unlike the type signature of grocer, the type signature of buyer has the effect annotation on the function arrow: { Choose: () => Bool, Throw: () => Zero | e }. This annotation is the effect type of the function, which asserts that this function must be invoked in a context that provides an interpretation of the operations Choose and Throw such that an invocation of Choose returns a Bool and an invocation of Throw never returns (its type is uninhabited so it cannot possibly return). The effect variable e can be instantiated with other effects, enabling effect polymorphism.

We now restate the example from the introduction using the buyer function.

links> {
  handle ({ var c = grocer();
            buyer(c) }) {
    case <Throw>             ->  ()
    case <Choose => resume>  ->  resume(true); resume(false)
  }
};

What happens when we run this code? The resumption function supplied to the handler for Choose at runtime is the following function.

fun resume(b) {
  handle ({
    var f = if (b) then Apple else Banana;
    var c = send(f, c);
    var (p, c) = receive(c);
    if (p > 42) throw()
    else ();
    var c = send(6, c);
    close(c)
  }) {
    case <Throw>             ->  ()
    case <Choose => resume>  ->  resume(true); resume(false)
  }
}

It uses the channel endpoint c from the environment. By invoking resume twice, the channel endpoint c is duplicated. Invoking the channel once leaves it closed. Resuming the continuation again leads to a runtime error, as a number cannot be sent along a closed channel endpoint.

This is unfortunate as it means that the type system of Links is unsound, leading to a stark violation of Milner’s slogan: “well-typed programs cannot go wrong”! How come the linear type system of Links did not detect this bug?

One answer is that conventional linear type systems only track value linearity, that is, linearity of primitive values, pairs, functions, etc. These values exist in the source code and are guaranteed to be used linearly. However, the resumption function resume has no static representation in the source code in the form of a function; it is a genuine dynamic entity created at runtime.

Another, essentially equivalent, answer is that conventional linear type systems assume that each continuation is invoked exactly once. This is true for most common programming language features, but false in the presence of unrestricted effect handlers as they provide first-class continuations which may be invoked more than once or not at all.

Of course, it is possible to side-step the problem by simply restricting effect handlers to be single-shot, but we seek to restore soundness without imposing such restrictions. In order to soundly handle linearity we describe how to extend linear type systems to track control-flow linearity .

Tracking Control-Flow Linearity

The key idea is to not only classify values as either linear or unlimited, but also to classify effectful operations as either control-flow-linear or control-flow-unlimited.

  • Control-flow-linear operation — its continuation must be resumed exactly once.

  • Control-flow-unlimited operation — its continuation can be resumed any number of times.

We extend the type system of Links to track control-flow linearity. With our new extension on (enabled with the command line flag --track-control-flow-linearity), the buyer is ill-typed with the following error message.

Type error: Variable c of linear type !(Fruit).?(Int).!(Int).End is used in a non-linear continuation.
In expression: c.

This type error comes from the second line of the function body of buyer, where we use the linear channel endpoint c in the continuation of the Choose operation invoked on the first line. The signature () => Bool indicates that Choose is a control-flow-unlimited operation, which means that its continuation cannot capture any linear values. We may amend the signature to () =@ Bool to indicate that Choose is a control-flow-linear operation. Our extended type system and type inference algorithm guarantees that linear resources can only be used in the continuations of control-flow-linear operations. Consequently, the Choose operation in buyer must be control-flow linear as we use the channel endpoint c after invoking Choose. The modified version of buyer with tracking for control-flow linearity is as follows.

sig buyer : (!Fruit.?Int.!Int.End) {Choose: () =@ Bool, Throw: () =@ Zero | e::Lin }~> ()
fun buyer(c) {
  xlin;
  var f = if (lindo Choose) Apple else Banana;
  var c = send(f, c);
  var (p, c) = receive(c);
  if (p > 42) switch (lindo Throw) { }
  else ();
  var c = send(6, c);
  close(c)
}

We make several other changes to buyer in addition to the operation signature of Choose. First, we inline the definition of the throw function and use the keyword lindo to invoke control-flow linear operations Choose and Throw. Second, we add the the kind annotation e::Lin in the effect type to assert that e is a control-flow-linear effect variable, guaranteeing that any other potential effects must also be control-flow linear. Third, in order to have sound and predictable type inference, we assume by default that all operations are allowed to be control-flow unlimited, and no linear resources can be used. In order to use linear resources, we need to use the xlin keyword which forces all operations in the current lexical scope to be control-flow linear.

If we try to type-check the program with just these amendments to buyer in place, we now see another type error, complaining that the receive on the second line of grocer should take a linear channel, whereas c is inferred to be unlimited. This is because we cannot use linear resources with the default unlimited control-flow.

As with buyer, we must also enable linear control-flow using xlin as a linear channel endpoint is used in the function body.

sig grocer : () { | e::Lin }~> !Fruit.?Int.!Int.End
fun grocer() {
  xlin;
  fork(fun(c) {
    xlin;
    var (f, c) = receive(c);
    var c = send(fruitPrice(f), c);
    var (i, c) = receive(c);
    println(intToString(i) ^^ fruitToString(f));
    close(c)
  })
}

Having fixed both buyer and grocer let us try to run them with our original handlers (not forgetting to enable linear control-flow with xlin).

links> {
  handle({ xlin; var c = grocer(); buyer(c) }) {
    case <Throw>             ->  ()
    case <Choose => resume>  ->  resume(true); resume(false)
  }
};
Type error: the effect type of the input to the handler is
    `{Choose:() =@ Bool,Throw: () =@ Zero, ...}'
while the handler handles effects
    `{Choose:() => Bool,Throw: () => Zero, ...}'

We now have a type error due to a mismatch between effect types. This is because control-flow linear operations must be handled by linear handler clauses whose syntax takes the form case <Choose =@ resume> -> .... Making this change, we still get a type error.

links> {
  handle({ xlin; var c = grocer(); buyer(c) }) {
    case <Throw  =@ resume>  ->  ()
    case <Choose =@ resume>  ->  resume(true); resume(false)
  }
};
Type error: Variable resume of linear type ... is used in a non-linear continuation.
In expression: resume.

This particular type error arises because the continuation of a linear handler clause is given a linear type. So the variable resume is linear in the Choose clause, but we have not added the necessary xlin annotation at the beginning of the clause. However, if we do so then we get another type error because the linear variable resume is used twice. Moreover, if we fix the Choose clause by deleting one of the calls to resume then we get a further type error, this time in the Throw clause where the linear variable resume is not used at all.

All of the changes we made to the program up to now were solely about ensuring that the program type-checks. They did not affect the dynamic semantics at all. Control-flow linearity enabled us to discover that our program is fundamentally unsound and to pinpoint exactly where the program violates soundness: it is unsound to use a continuation that captures linear values zero or more than one times.

Having isolated the bug in the logic of the original program, how might we now change its semantics to fix the bug?

It is easy to make the handler clause for Choose linear. We can, for instance, simply always pick the first branch.

    case <Choose =@ resume>  ->  xlin; resume(true)

However, Throw is intrinsically control-flow unlimited. We cannot resume it as its type signature is () => Zero. One way to fix the original program is to elide the use of Throw completely by replacing a request for 6 fruit with a request for 0 fruit.

  sig buyer' : (!Fruit.?Int.!Int.End) {Choose:() =@ Bool | e::Lin }~> ()
  fun buyer'(c) {
    xlin;
    var f = if (lindo Choose) Apple else Banana;
    var c = send(f, c);
    var (p, c) = receive(c);
    if (p > 42) {
      var c = send(0, c);
      close(c)
    }
    else {
      var c = send(6, c);
      close(c)
    }
  }
links> {
    handle({ xlin; var c = grocer(); buyer'(c) }) {
      case <Choose =@ resume>  ->  xlin; resume(true)
    }
};
0 apple

Now the code type-checks and runs successfully. We have used control-flow linearity to discover and fix the original type soundness bug and soundly handled linearity in Links!

Towards More Expressive Control-Flow Linearity

We require syntactic annotations in Links in order to obtain a deterministic type inference algorithm which tracks both value linearity and control-flow linearity, including the lindo and xlin keywords. Though we believe that these annotations are mostly acceptable and provide useful information in practice, they can still be annoying. In particular they can interfere with reusability, as we may now need to provide several versions of the same function. For instance, consider a simple verbose identity function which prints "id" before returning its parameter.

fun verboseId(x) {do Print("id"); x}

With xlin and lindo, we can define several different variants of this function, which do not subsume one another.

sig verboseId : (a) { Print : (String) => () | e }-> a
fun verboseId(x) {do Print("id"); x}
sig verboseId : (a) { Print : (String) =@ () | e }-> a
fun verboseId(x) {lindo Print("id"); x}
sig verboseId : (a::Any) { Print : (String) =@ () | e::Lin }-> a::Any
fun verboseId(x) {xlin; lindo Print("id"); x}

The kind annotation Any here indicates that a can be instantiated with linear types. With qualified types we can combine all of these three versions into a single one and completely avoid the syntactic overheads of xlin and lindo.

sig verboseId : (a) { Print : (String) =>ϕ () | ρ }-> a with (a <= ϕ, a <= ρ)
fun verboseId(x) {do Print("id"); x}

Now types may contain linearity constraints on type variables appearing in them. The =>ϕ means that the Print operation is polymorphic over its control-flow linearity ϕ, a linearity variable. The constraint (a <= ϕ, a <= ρ) ensures that the value type variable a is less linear than the linearity variable ϕ and the control-flow linearity of the effect variable ρ. In other words, when ϕ or ρ is control-flow unlimited, a must be unlimited as well. This is the essential constraint shared by all three previous versions, which suffices to guarantee linearity safety.

It may seem complicated to include constraints in types. What exactly do we gain from using qualified types for control-flow linearity? The most obvious advantage is that we no longer need any of the syntactic annotations at all. For example, the grocer and buyer example from the introduction can be made well-typed without the need to insert xlin anywhere, providing we ensure that handlers for Throw and Choose are single-shot.

In our POPL 2024 paper, we formalise such a qualified type system along with a sound and complete type inference algorithm. We leave an implementation of this qualified type system as future work.

Control-flow linearity facilities the harmonious coexistence of linear types and effect handlers within the same programming language. Picture by Xueying Qin.

Picture by Xueying Qin

The Paper

Our POPL 2024 paper describes in full technical detail how to soundly handle linearity. In particular it describes:

  • a System F-style core calculus equipped with linear types, and effect type system, and effect handlers along with proofs of syntactic type soundness and a semantic linear safety property;
  • the Links implementation, which is based on this core calculus, and fixes a long-standing type-soundness bug;
  • and an ML-style core calculus inspired by Quill and Rose, based on qualified types along with proofs of soundness and completeness of type inference.

Acknowledgements: We would like to thank Xueying Qin for providing the two figures featured in this blog post.

About the authors: Wenhao Tang is a PhD student at the Laboratory for Foundations of Computer Science in the School of Informatics at The University of Edinburgh. He is interested in the static semantics of functional programming languages, with a focus on type-and-effect systems. Daniel Hillerström is a senior researcher at the Computing Systems Laboratory in the Zurich Research Center at Huawei Technologies Switzerland. His research focuses on the operational foundations of effect handler oriented programming. Sam Lindley is a reader in programming language design and implementation at the Laboratory for Foundations of Computer Science in the School of Informatics at The University of Edinburgh. He holds a UKRI Future Leaders Fellowship in Effect Handler Oriented Programming. J. Garrett Morris is assistant professor and Emeriti Faculty Scholar in the Department of Computer Science at the University of Iowa. His research focuses on the development of type systems for modularity and extensibility in higher-order functional programming languages. He is a 2021 recipient of the NSF CAREER award.

Disclaimer: These posts are written by individual contributors to share their thoughts on the SIGPLAN blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGPLAN or its parent organization, ACM.