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.