Skip to content

Control flow linearity

Jump to bottom
Wenhao Tang edited this page Oct 3, 2023 · 5 revisions

Control-Flow Linearity (CFL)

The CFL extension tracks control-flow linearity, which enables sound combination of linear types (session types) and multi-shot effect handlers. Enable the feature of tracking control-flow linearity by passing the flag --control-flow-linearity. It automatically enables the flag --enable-handlers.

New Constructs

The CFL extension introduces the following new constructs:

  • Type syntax A =@ B represents signatures for control-flow-linear operations (A => B for control-flow-unlimited operations)
  • Kind syntax Lin represents kinds for control-flow-linear effect variables (Any for effect variables with no linearity restriction)
  • Term syntax lindo L invokes control-flow-linear operations (do U for control-flow-unlimtied operations)
  • Term syntax case <L =@ r> -> M handles control-flow-linear operations L (case <U => r> -> M for control-flow-unlimited operations)
  • Term syntax xlin switches the current control-flow linearity to linear (by default, the control-flow linearity is unlimited)

Understanding CFL in Links

To understand what CFL exactly means in Links, we need to know how the effect system of Links works. Links adopts an effect system based on Rémy-style row polymorphism and supports ML-style type inference of it. As a result, the effect types of sequenced computations are unified. We introduce the concept effect scope to mean the scope where computations share effects (i.e., have the same effect types). There are only two cases that new effect scopes are created:

  • Function bodies (closures) hold their own effect scopes.
  • Computations being handled (the M in handle M {...}) have their own effect scopes, but also share those unhandled effects with computations outside the handler.

All operations invoked in the same effect scope have the same control-flow linearity. By default, the control-flow linearity of every effect scope is unlimited. We are allowed to use both control-flow-linear and control-flow-unlimited operations, but only unlimited value variables. We can switch the control-flow linearity of the current effect scope to linear by xlin. Then, we are allowed to use both unlimited and linear value variables, but only control-flow-linear operations. Note that switching the control-flow linearity to linear is irreversible since control-flow-linear effect row variables can never be made unlimited. All invocations of unlimited operations in a control-flow-linear effect scope (even before xlin) would cause type errors.

Examples

We enter REPL with CFL enabled:

> linx --enable-handlers --track-control-flow-linearity

  • Invoke a control-flow-linear operation Choose in a control-flow-linear context:

    links> fun g1() {xlin; if (lindo Choose) 42 else 84};
g1 = fun : () {Choose:() =@ Bool|_::Lin}-> Int

    We use xlin to switch the current control-flow linearity to linear. The anonymous effect row variable _ has kind Lin which can only be unified with control-flow-linear operations.

  • Invoke a control-flow-linear operation Choose in a control-flow-unlimited context:

    links> fun g2() {if (lindo Choose) 42 else 84};
g2 = fun : () {Choose:() =@ Bool|_}-> Int

    It is sound to invoke control-flow-linear operations in control-flow-unlimited contexts. Without kind annotation, the anonymous effect row variable _ has kind Any by default which can be unified with any operations.

  • Mix control-flow-linear and control-flow-unlimited operations in a control-flow-unlimited context:

    links> fun g3() {if (lindo Choose) do Print("42") else do Print ("84")};
g3 = fun : () {Choose:() =@ Bool,Print:(String) => a|_}-> a

  • Handle control-flow-linear operations:

    links> handle (g1()) {case <Choose =@ r> -> xlin; r(true)};
42 : Int
links> handle (g2()) {case <Choose =@ r> -> xlin; r(true)};
42 : Int
links> handle (handle (g3()) {case <Print(s) => r> -> println(s); r(())})
       {case <Choose =@ r> -> xlin; r(true)}
42
() : ()

    We write case <Choose =@ r> -> ... for the handler clauses of the control-flow-linear operation Choose. The operation clauses must match the control-flow linearity of operations. Otherwise, we get a type error:

    links> handle (g1()) {case <Choose => r> -> r(true) + r(false)};
<stdin>:1: Type error: The effect type of an input to a handle should match the type of its computation patterns, but the expression
    `g1()'
has effect type
    `{Choose:() =@ Bool|a}'
while the handler handles effects
    `{Choose:() => Bool,wild:()|b::Any}'
In expression: handle (g1()) {case <Choose => r> -> r(true) + r(false)}.

    The continuation function r bound by Choose =@ r is given a linear function type and must be used exactly once in a control-flow-linear context (enabled by xlin). Otherwise, we get type errors:

    links> handle (g1()) {case <Choose =@ r> -> r(true) + r(false)};
<stdin>:1: Type error: Variable r has linear type
    `(Bool) {}~@ Int'
but is used 2 times.
In expression: handle (g1()) {case <Choose =@ r> -> r(true) + r(false)}.

  • Use linear resources in a control-flow-linear context:

    links> fun(ch) {xlin; var x = if (lindo Choose) 42 else 84; close(send(x,ch))};
fun : (!(Int).End) {Choose:() =@ Bool|_::Lin}~> ()

    The linear channel ch must be used in control-flow-linear contexts. Otherwise, we get a type error complaining that the variable ch has an unlimited type which cannot be unified with a session type:

    links> fun(ch) {var x = if (lindo Choose) 42 else 84; close(send(x,ch))};
<stdin>:1: Type error: The function
    `send'
has type
    `(Int, !(Int).a::Session) ~b~> a::Session'
while the arguments passed to it have types
    `Int'
and
    `c::(Unl,Mono)'
...

  • Handle control-flow-unlimited operations fully before entering control-flow-linear contexts:

    links> fun(ch) { xlin;
                 var x = handle ({if (do Choose) 42 else 84})
                         {case <Choose => r> -> r(true) + r(false)};
                 close(send(x,ch)) };
fun : (!(Int).End) {Choose{_::Lin}|_::Lin}~> ()

    Note that after handling, the presence variable of Choose and row variable are both control-flow-linear because the handler is in a control-flow-linear context.

  • Explicit quantifiers for effect row variables with control-flow linearity:

    links> sig f:forall e::Row(Any). () {Get:() => Int|e}-> Int fun f() {do Get}
f = fun : () {Get:() => Int|_}-> Int

    When writing explicit quantifiers, we should explicitly annotate the control-flow linearity of effect row variables in their kinds using e::Row(Lin) or e::Row(Any). If the subkind is not specified, it means Lin instead of Any for backwards compatibility (because row variables are used by both effect types and variant / record types in Links). It is meaningful future work to explicitly separate value row variables and effect row variables in Links.

Design choices

It is necessary to have xlin for the same reason of having linfun in Links. For example, neither of the following functions has a more general type than the other one.

links> fun(x) {lindo L; x};
fun : (a) {L:() =@ ()|_}-> a
links> fun(x) {xlin; lindo L; x};
fun : (a::Any) {L:() =@ ()|_::Lin}-> a::Any

Compatibility

  • This extension passes all previous tests with the flag disabled.
  • Since this extension more focuses on the compatibility with the effect handler extension of Links, it passes all previous effect handler tests with the flag enabled, including
    • /tests/handlers_with_cfl_on.tests, and
    • /tests/typecheck_examples_with_cfl_on.tests.
  • For other tests especially those use session types, since this extension changes some parsing/printing behaviours and does not allow linear resources by default, appropriate changes are required to make it pass the tests with the flag enabled.
Clone this wiki locally