异常和状态

Control.App 主要是为了更容易管理有异常和状态的应用程序的常见情况。我们可以抛出和捕捉错误列表中列出的异常（ es 参数为 App ），并引入新的全局状态。

异常

List Error 是一个错误类型列表，可以使用以下函数抛出和捕获：

throw : HasErr err es => err -> App es a
catch : HasErr err es => App es a -> (err -> App es a) -> App es a

只要异常类型存在于错误列表 es 中，就可以使用 throw 和 catch 来抛出和捕获异常，如 HasErr 谓词所检查的那样（注意， Exception 是 HasErr 的同义词）：

data HasErr : Error -> List Error -> Type where
     Here : HasErr e (e :: es)
     There : HasErr e es -> HasErr e (e' :: es)

Exception : Error -> List Error -> Type
Exception = HasErr

最后，我们可以通过 handle 引入新的异常类型，运行可能会抛出异常的代码块，并处理任何异常：

handle : App (err :: e) a ->
         (onok : a -> App e b) ->
         (onerr : err -> App e b) -> App e b

添加状态

应用程序通常需要跟踪状态，我们在 App 中使用 Control.App 中定义的 State 类型支持这个原语：

data State : (tag : a) -> Type -> List Error -> Type

tag 只被用于区分不同的状态，在运行时是不需要，如用于访问和更新的 get 和 put 类型：

get : (0 tag : _) -> State tag t e => App {l} e t
put : (0 tag : _) -> State tag t e => (1 val : t) -> App {l} e ()

它们使用 auto-implicit 来隐式传递带有相关 tag 的 State ，因此我们仅通过标签来引用状态。在前面的 helloCount 中，我们使用了一个空类型 Counter 作为标签：

data Counter : Type where -- complete definition

错误列表 e 用来确保状态只在其被引入的错误列表中可用。状态是用 new 引入的：

new : t -> (1 p : State tag t e => App {l} e a) -> App {l} e a

请注意，这个类型告诉我们 new 用这个状态运行程序正好一次。然而，我们通常不直接使用 State 和 Exception ，而是使用接口来约束错误列表中允许的操作。在内部， State 是通过 IORef 实现的，这主要是出于性能的考虑。