Abilities and ability handlers

Abilities in function types

The general form for a function type in Unison isI ->{A} O,whereIis the input type of the function,Ois the output type, andAis the set ofability requirementsof the function. More generally, this can be any comma-separated list of types, likeI ->{A1,A2,A3} O.

A function type in Unison likeA -> Bis really syntactic sugar for a typeA ->{e} Bwhereeis some set of abilities, possibly empty. A function that definitely requires no abilities has a type likeA ->{} B(it has an empty set of abilities).

The typechecking rule for abilities

The general typechecking rule used for abilities is this: calls to functions requiring abilities{A1,A2}must be in a context whereat leastthe abilities{A1,A2}are available, otherwise the typechecker will complain with an ability check failure. Abilities can be made available using ahandleblock (discussed below) or with a type signature: so for instance, within the body of a functionText ->{IO} Nat,{IO}is available and therefore:

• We can call a functionf : Nat ->{} Nat,since the ability requirements of f are{}which is a subset the available{IO}abilities.
• We can also call a functiong : Text ->{IO} (),since the requirements ofgare{IO}which is a subset of the available{IO}abilities.

For functions accepting multiple arguments, it might seem we need a different rule, but the rule is the same: the body of the function can access the abilities attached to the corresponding function type in the signature. Here's an example that won't typecheck, since the function body must be pure according to the signature:

doesNotWork : Text ->{Exception,IO} Text ->{} Nat
doesNotWork arg1 arg2 =
  printLine "Does not work!"
  42

However, if we do theIObefore returning the pure function, it typechecks just fine:

doesWork : Text ->{IO, Exception} Text -> Nat
doesWork arg1 =
  printLine "Works great!"
  arg2 -> 42

For top-level definitions which aren't contained in a function body,they are required to be pure.For instance, this doesn't typecheck:

msg = printLine "hello"

But if we saymsg = '(printLine "Hello")that typechecks fine, since theprintLineis now inside a function body whose requirements inferred as{IO}(try it!).

🤓 This restriction on top level definitions needing to be pure might lifted in a future version of Unison.

Ability inference

When inferring ability requirements forf,the ability requirements become the union of all requirements for functions that can be called within the body of the function.

User-defined abilities

A user-defined ability is declared with anabilitydeclaration such as:

structural ability Store a

structural ability Store a where
  put : a ->{Store a} ()
  get : {Store a} a

Abilities need to be defined with either thestructuraloruniquekeyword. See the sections onunique typesandstructural-typesfor more detail on the difference.

This results in a new ability type constructorStorewhich takes a type argumenta.It also create two value-level constructors namedStore.getandStore.put.The idea is thatStore.getprovides the ability to "get" a value of typeafrom somewhere, andStore.putallows "putting" a value of typeasomewhere. Where exactly these values of typeawill be kept depends on the handler.

TheStoreconstructorsStore.getandStore.puthave the following types:

• Store.get : {Store a} a
• Store.put : a ->{Store a} ()

The type{Store v}means that the computation which results in that type requires aStore vability and cannot be executed except in the context of anability handlerthat provides the ability.

Ability handlers

A constructor{A} Tfor some abilityAand some typeT(or a function which uses such a constructor), can only be used in a scope where the abilityAis provided. Abilities are provided byhandleexpressions:

handle e with h

This expression giveseaccess to abilities handled by the functionh.Specifically, ifehas type{A} Tandhhas typeRequest A T -> R,thenhandle e with hhas typeR.The type constructorRequestis a special builtin provided by Unison which will pass arguments of typeRequest A Tto a handler for the abilityA.Note thathmustaccept an argument of typeRequest A Tto handleeof type{A} T- ultimately, a type error will result if an ability is required in a scope where it is not provided by an enclosing handle expression.

The examples in the next section should help clarify how ability handlers work.

Pattern matching on ability constructors

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_ -> ().