线性资源

我们已经介绍了 App 用于编写交互式程序，使用接口来限制允许哪些操作，但还没有看到 Path 参数的作用。其目的是限制程序何时可以抛出异常，以了解允许线性资源使用的位置。 App 的绑定运算符定义如下（不是通过 Monad ）：

data SafeBind : Path -> (l' : Path) -> Type where
     SafeSame : SafeBind l l
     SafeToThrow : SafeBind NoThrow MayThrow

(>>=) : SafeBind l l' =>
        App {l} e a -> (a -> App {l=l'} e b) -> App {l=l'} e b

这种类型背后的直觉是，当对两个 App 程序进行排序时：

如果第一个动作可能抛出异常，那么整个程序就可能会抛出异常。
如果第一个动作不能抛出异常，那么第二个动作仍然可以抛出，整个程序也就会抛出异常。
如果两个动作都不会抛出异常，则整个程序都不会抛出异常。

类型中详细的原因是它对具有不同 Path 的程序进行排序很有用，但在这样做时，我们必须准确计算得到的 Path 。然后，如果我们想用线性变量对子程序进行排序，我们可以使用另一种绑定运算符来保证只运行一次延续：

bindL : App {l=NoThrow} e a ->
        (1 k : a -> App {l} e b) -> App {l} e b

为了说明 bindL 的必要性，我们可以尝试编写一个程序来跟踪安全数据存储的状态，这需要在读取数据之前登录。

示例：需要登录的数据存储

许多软件组件依赖于某种形式的状态，并且可能存在仅在特定状态下有效的操作。例如，考虑一个安全的数据存储，用户必须在其中登录才能访问某些秘密数据。该系统可以处于以下两种状态之一：

LoggedIn ，允许用户在其中读取秘密
LoggedOut ，用户无权访问机密

我们可以提供登录、注销和读取数据的命令，如下图所示：

login 命令，如果成功，将整个系统状态从 LoggedOut 移动到 LoggedIn 。 logout 命令将状态从 LoggedIn 移动到 LoggedOut 。最重要的是， readSecret 命令仅在系统处于 LoggedIn 状态时才有效。

我们可以使用线性类型的函数来表示状态转换。首先，我们定义一个用于连接和断开商店的接口：

interface StoreI e where
    connect : (1 prog : (1 d : Store LoggedOut) ->
              App {l} e ()) -> App {l} e ()
    disconnect : (1 d : Store LoggedOut) -> App {l} e ()

如对 l 的泛化所示，connect 和 disconnect 都不会抛出异常。建立连接后，我们可以使用以下函数直接访问资源：

data Res : (a : Type) -> (a -> Type) -> Type where
     (#) : (val : a) -> (1 resource : r val) -> Res a r

login : (1 s : Store LoggedOut) -> (password : String) ->
        Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut))
logout : (1 s : Store LoggedIn) -> Store LoggedOut
readSecret : (1 s : Store LoggedIn) ->
             Res String (const (Store LoggedIn))

Res 在 Prelude 中定义，因为它非常常用。它是一种依赖对（dependent pair）类型，将一个值与线性资源关联起来。为便于本介绍性示例，其他定义暂且抽象化处理。

下面的代码清单展示了一个完整的存储访问程序：它会读取密码，若密码正确则访问存储并打印机密数据。它通过 let (>>=) = bindL 和 (>>) = seqL 在本地重新定义 do-notation。

storeProg : Has [Console, StoreI] e => App e ()
storeProg = let (>>=) = bindL
                (>>) = seqL in
      do putStr "Password: "
         password <- getStr
         connect $ \s =>
           do let True # s = login s password
                | False # s => do putStrLn "Wrong password"
                                  disconnect s
              let str # s = readSecret s
              putStrLn $ "Secret: " ++ show str
              let s = logout s
              disconnect s

如果省略 let (>>=) = bindL，将会使用默认的 (>>=) 运算符，这允许延续（continuation）被多次执行，这意味着 s 无法保证被线性访问，storeProg 也无法通过类型检查（(>>) = bindIg 同理）。我们可以安全地使用 getStr 和 putStr，因为它们的类型中的 Path 参数保证不会抛出异常。

App1：线性接口

通过添加 bindL 函数，使我们可以在本地重新绑定 (>>=) 运算符，从而将现有的线性资源程序与 App 中的操作结合起来——至少是那些不会抛出异常的操作。当然，如果能与 App 更直接地互操作会更好。定义接口的一个优点是可以为不同上下文提供多种实现，但我们的数据存储实现是通过原始函数（无论如何都未定义）来访问存储的。

为了便于控制线性资源，Control.App 提供了一个可选的参数化类型 App1：

data App1 : {default One u : Usage} ->
            (es : List Error) -> Type -> Type

不需要 Path 参数，因为线性程序永远不会抛出异常。Usage 参数说明返回的值是只使用一次还是可以不受限制地使用，App1 中的默认值是只使用一次：

data Usage = One | Any

与 App 的主要区别在于 (>>=) 运算符：根据第一个动作的用法，由延续（continuation）绑定的变量具有不同的多重性（multiplicity）：

Cont1Type : Usage -> Type -> Usage -> List Error -> Type -> Type
Cont1Type One a u e b = (1 x : a) -> App1 {u} e b
Cont1Type Any a u e b = (x : a) -> App1 {u} e b

(>>=) : {u : _} -> (1 act : App1 {u} e a) ->
        (1 k : Cont1Type u a u' e b) -> App1 {u=u'} e b

如果第一个 App1 程序的用法为 One，Cont1Type 返回一个线性使用参数的延续（continuation）；否则，返回一个参数用法不受限制的延续。无论哪种情况，由于作用域内可能存在线性资源，延续都只会被执行一次，并且不会抛出异常。

使用 App1，我们可以在单个接口中定义所有数据存储操作，如下代码清单所示。除 disconnect 外，每个操作都返回一个线性资源。

interface StoreI e where
  connect : App1 e (Store LoggedOut)
  login : (1 d : Store LoggedOut) -> (password : String) ->
          App1 e (Res Bool (\ok => Store (if ok then LoggedIn
                                                else LoggedOut))
  logout : (1 d : Store LoggedIn) -> App1 e (Store LoggedOut)
  readSecret : (1 d : Store LoggedIn) ->
               App1 e (Res String (const (Store LoggedIn)))
  disconnect : (1 d : Store LoggedOut) -> App {l} e ()

我们可以在 App 和 App1 之间显式地进行转换：

app : (1 p : App {l=NoThrow} e a) -> App1 {u=Any} e a
app1 : (1 p : App1 {u=Any} e a) -> App {l} e a

我们可以在 App1 中使用 app 运行一个 App 程序，前提是它保证不会抛出异常。同理，也可以在 App 中用 app1 运行 App1 程序，前提是其返回值可以不受限制地使用。例如，可以这样写：

storeProg : Has [Console, StoreI] e => App e ()
storeProg = app1 $ do
     store <- connect
     app $ putStr "Password: "
     ?what_next

这里用 app1 表明程序主体是线性的，再用 app 表明 putStr 操作属于 App。我们可以通过检查空洞（hole）``what_next``，看到 connect 返回一个线性资源，这也说明我们正运行在 App1 内部：

 0 e : List Type
 1 store : Store LoggedOut
-------------------------------------
what_next : App1 e ()

为完整起见，接口的一种实现方式如下，使用了硬编码的密码和内部数据：

Has [Console] e => StoreI e where
  connect
      = do app $ putStrLn "Connect"
           pure1 (MkStore "xyzzy")

  login (MkStore str) pwd
      = if pwd == "Mornington Crescent"
           then pure1 (True # MkStore str)
           else pure1 (False # MkStore str)
  logout (MkStore str) = pure1 (MkStore str)
  readSecret (MkStore str) = pure1 (str # MkStore str)

  disconnect (MkStore _)
      = putStrLn "Disconnect"

然后我们可以在 main 中运行它：

main : IO ()
main = run storeProg