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 constructorAwith type parametersp_1throughp_n,and request constructorsRequest_1throughRequest_n

Examples

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