Exceptions and State
Control.App
is primarily intended to make it easier to manage the common
cases of applications with exceptions and state. We can throw and catch
exceptions listed in the list of errors (the es
parameter to App
) and
introduce new global state.
Exceptions
The List Error
is a list of error types, usable via the
Exception
interface defined in Control.App
:
interface Exception err e where
throw : err -> App e a
catch : App e a -> (err -> App e a) -> App e a
We can use throw
and catch
for some exception type
err
as long as the exception type exists in the list of errors. This is
checked with the HasErr
predicate, also defined in Control.App
:
data HasErr : Error -> List Error -> Type where
Here : HasErr e (e :: es)
There : HasErr e es -> HasErr e (e' :: es)
HasErr err es => Exception err es where ...
Note the HasErr
constraint on Exception
: this is one place
where it is notationally convenient that the auto
implicit mechanism
and the interface resolution mechanism are identical in Idris 2.
Finally, we can introduce new exception types via handle
, which runs a
block of code which might throw, handling any exceptions:
handle : App (err :: e) a ->
(onok : a -> App e b) ->
(onerr : err -> App e b) -> App e b
Adding State
Applications will typically need to keep track of state, and we support
this primitively in App
using a State
type, defined in
Control.App
:
data State : (tag : a) -> Type -> List Error -> Type
The tag
is used purely to distinguish between different states,
and is not required at run-time, as explicitly stated in the types of
get
and put
, which are used to access and update a state:
get : (0 tag : _) -> State tag t e => App {l} e t
put : (0 tag : _) -> State tag t e => (1 val : t) -> App {l} e ()
These use an auto
-implicit to pass around
a State
with the relevant tag
implicitly, so we refer
to states by tag alone. In helloCount
earlier, we used an empty type
Counter
as the tag:
data Counter : Type where -- complete definition
The list of errors e
is used to ensure that
states are only usable in the list of errors in which they are introduced.
States are introduced using new
:
new : t -> (1 p : State tag t e => App {l} e a) -> App {l} e a
Note that the type tells us new
runs the program with the state
exactly once.
Rather than using State
and Exception
directly, however,
we typically use interfaces to constrain the operations which are allowed
in a list of errors. Internally, State
is implemented via an
IORef
, primarily for performance reasons.