APP 介绍

App 声明在模块 Control.App 中，它是 base 库的一部分。它的参数是一个隐含的 Path （说明程序的执行路径是线性的还是可能抛出异常），它有一个 default 值，程序可能会抛出一个 List Error （一个可以抛出的异常类型列表， Error 是 Type 的同义词）：

data App : {default MayThrow l : Path} ->
           (es : List Error) -> Type -> Type

它的作用与 IO 相同，但支持抛出和捕获异常，并允许我们定义更多的由错误列表 es 参数化的约束性接口。例如，一个支持控制台IO的程序：

hello : Console es => App es ()
hello = putStrLn "Hello, App world!"

我们可以在一个完整的程序中使用它，如下所示：

module Main

import Control.App
import Control.App.Console

hello : Console es => App es ()
hello = putStrLn "Hello, App world!"

main : IO ()
main = run hello

或者，一个支持控制台IO的程序，携带一个 Int 的状态，标记为 Counter ：

data Counter : Type where

helloCount : (Console es, State Counter Int es) => App es ()
helloCount = do c <- get Counter
                put Counter (c + 1)
                putStrLn "Hello, counting world"
                c <- get Counter
                putStrLn ("Counter " ++ show c)

为了将其作为一个完整程序的一部分来运行，我们需要初始化状态。

main : IO ()
main = run (new 93 helloCount)

为了方便起见，我们可以一次性列出多个接口，使用 Control.App 中定义的函数 Has 来计算接口约束：

helloCount : Has [Console, State Counter Int] es => App es ()

0 Has : List (a -> Type) -> a -> Type
Has [] es = ()
Has (e :: es') es = (e es, Has es' es)

Path 的目的是说明一个程序是否可以抛出异常，这样我们就可以知道在哪里引用线性资源是安全的。它被声明如下：

data Path = MayThrow | NoThrow

App 的类型中 MayThrow 是默认的。我们希望这是最常见的情况。毕竟，现实中，大多数操作都有可能的失败模式，特别是那些与外部世界交互的操作。

0 在 Has 的声明中表示它只能在一个被擦除的上下文中运行，所以它在运行时永远不会被运行。为了在 IO 内运行一个 App ，我们使用一个初始错误列表 Init （记住 Error 是 Type 的同义词）：

Init : List Error
Init = [AppHasIO]

run : App {l} Init a -> IO a

通过 l 对 Path 参数进行泛化，意味着我们可以为任何应用程序调用 run，无论 Path 是 NoThrow 还是 MayThrow。但在实践中，所有传给 run 的应用程序都不会在顶层抛出异常，因为唯一可用的异常类型是 AppHasIO，这是一个空数据类型（它没有任何值）。任何异常都会在 App 内部被引入和处理。