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.put : a ->{Store a} ()
  lib.base.abilities.Store.get : {Store a} a