Pattern matching on ability constructors

Each constructor of an ability corresponds with a pattern that can be used for pattern matching in ability handlers. The general form of such a pattern is:

{A.c p_1 p_2 p_n -> k}

Where A is the name of the ability, c is the name of the constructor, p_1 through p_n are patterns matching the arguments to the constructor, and k is a continuation for the program. If the value matching the pattern has type Request A T and the constructor of that value had type X ->{A} Y, then k has type Y -> {A} T.

The continuation will always be a function accepting the return value of the ability constructor, and the body of this function is the remainder of the handle .. with block immediately following the call to the constructor. See below for an example.

A handler can choose to call the continuation or not, or to call it multiple times. For example, a handler can ignore the continuation in order to handle an ability that aborts the execution of the program:

structural ability Abort

structural ability Abort where
  lib.base.abilities.Abort.abort : {Abort} a

toDefault!.handler : '{g} a -> Request {Abort} a ->{g} a

toDefault!.handler : '{g} a -> Request {Abort} a ->{g} a
toDefault!.handler default = cases
  { a }                -> a
  { Abort.abort -> _ } -> default()

use Nat +
p : Nat
p =
  handle
    (_eta -> let
      x = 4
      Abort.abort
      x + 2) ()
  with toDefault!.handler do 0
p
⧨
0

If we remove the Abort.abort call in the program p, it evaluates to 6.

Note that although the ability constructor is given the signature abort : (), its actual type is {Abort} ().

The pattern { Abort.abort -> _ } matches when the Abort.abort call in p occurs. This pattern ignores its continuation since it will not invoke it (which is how it aborts the program). The continuation at this point is the expression _ -> x + 2.

The pattern { x } matches the case where the computation is pure (makes no further requests for the Abort ability and the continuation is empty). A pattern match on a Request is not complete unless this case is handled.

When a handler calls the continuation, it needs describe how the ability is provided in the continuation of the program, usually with a recursive call, like this:

use base Request

structural ability Store v where
  get : v
  put : v -> ()

storeHandler : v -> Request (Store v) a -> a
storeHandler storedValue = cases
  {Store.get -> k} ->
    handle k storedValue with storeHandler storedValue
  {Store.put v -> k} ->
    handle k () with storeHandler v
  {a} -> a

Note that the storeHandler has a with clause that uses storeHandler itself to handle the Request`s made by the continuation. So it’s a recursive definition. The initial "stored value" of type v is given to the handler in its argument named storedValue, and the changing value is captured by the fact that different values are passed to each recursive invocation of the handler.

In the pattern for Store.get, the continuation k expects a v, since the return type of Store.get is v. In the pattern for Store.put, the continuation k expects (), which is the return type of Store.put.

It's worth noting that this is a mutual recursion between storeHandler and the various continuations (all named k). This is no cause for concern, as they call each other in tail position and the Unison compiler performs tail call elimination.

An example use of the above handler:

modifyStore : (v -> v) ->{Store v} ()
modifyStore f =
  v = get
  put (f v)

Here, when the handler receives Store.get, the continuation is v -> Store.put (f v). When the handler receives Store.put, the continuation is _ -> ().