Pattern matching on ability constructors · Unison programming language

Each constructor of an ability corresponds with apatternthat 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}

WhereAis the name of the ability,cis the name of the constructor,p_1throughp_nare patterns matching the arguments to the constructor, andkis acontinuationfor the program. If the value matching the pattern has typeRequest A Tand the constructor of that value had typeX ->{A} Y,thenkhas typeY -> {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 thehandle .. withblock 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 abort : {Abort} a

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

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

p : Nat
p =
  handle
    !(do
      use Nat +
      x = 4
      abort
      x + 2)
  with toDefault!.handler '0
p⧨0

If we remove theabortcall in the programp,it evaluates to6.

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

The pattern{ Abort.abort -> _ }matches when theabortcall inpoccurs. 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 theAbortability and the continuation is empty). A pattern match on aabilities.Requestis 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 thestoreHandlerhas awithclause that usesstoreHandleritself to handle theRequest`smade by the continuation. So it’s a recursive definition. The initial "stored value" of typevis given to the handler in its argument namedstoredValue,and the changing value is captured by the fact that different values are passed to each recursive invocation of the handler.

In the pattern forStore.get,the continuationkexpects av,since the return type ofStore.getisv.In the pattern forStore.put,the continuationkexpects(),which is the return type ofStore.put.

It's worth noting that this is a mutual recursion betweenstoreHandlerand the various continuations (all namedk).This is no cause for concern, as they call each other in tail position and the Unison compiler performstail 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 receivesStore.get,the continuation isv -> Store.put (f v).When the handler receivesStore.put,the continuation is_ -> ().