Ability declaration

The ability declaration defines the name and the request operations of an ability. It also specifies if an ability is unique by its name or structural.

It takes the following general form:

unique|structural ability A p_1 p_2 … p_n where
    Request_1 : Type_1
    Request_2 : Type_2
    Request_n : Type_n

This declares an ability type constructor A with type parameters p_1 through p_n, and request constructors Request_1 through Request_n

Examples

structural ability Throw e
structural ability Throw e where
  lib.base.abilities.Throw.throw : e ->{Throw e} a
structural ability Store a
structural ability Store a where
  lib.base.abilities.Store.get : {Store a} a
  lib.base.abilities.Store.put : a ->{Store a} ()

Indexed abilities

Each request constructor can specialize the ability's type parameters in its ability requirement. Write the indexed ability explicitly in the operation's type:

unique ability Eff a where
  emitNat : Nat ->{Eff Nat} ()
  emitBool : Boolean ->{Eff Boolean} ()

emitNat requires Eff Nat, while emitBool requires Eff Boolean. The index is independent of the operation's return type; both operations above return ().

Matching an operation in a handler refines the corresponding ability's index within that branch. For a handler with signature Request {Eff a} r -> Optional a, the emitNat branch can return Some n, where n : Nat, and the emitBool branch can return Some b, where b : Boolean.

When the handled index is concrete, operations incompatible with that index need not be covered. A handler for Request {Eff Nat} r needs an emitNat case and a normal-completion case, but no emitBool case. When a handler handles multiple abilities, refining one ability's index leaves the other abilities unchanged.

See indexed abilities in the language guide for complete handlers and an explanation of how continuations behave.