User-defined abilities

A user-defined ability is declared with an ability declaration such as:

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

Abilities need to be defined with either the structural or unique keyword. See the sections on unique types and structural-types for more detail on the difference.

This results in a new ability type constructor Store which takes a type argument a. It also create two value-level constructors named Store.get and Store.put. The idea is that Store.get provides the ability to "get" a value of type a from somewhere, and Store.put allows "putting" a value of type a somewhere. Where exactly these values of type a will be kept depends on the handler.

The Store constructors Store.get and Store.put have 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 a Store v ability and cannot be executed except in the context of an ability handler that provides the ability.