定义接口

Control.App 提供的运行 App 的唯一方法是通过 run 函数，它接收一个具体的错误列表 Init 。对这个错误列表的所有具体扩展都是通过 handle 以引入一个新的异常，或者 new 以引入一个新状态。为了有效地组成 App 程序，而不是笼统地引入具体的异常和状态，我们为在特定错误列表中工作的操作集合定义接口。

Console I/O 示例

我们已经看到了一个使用 Console 接口的初始示例，它在 Control.App.Console 中声明如下：

interface Console e where
  putChar : Char -> App {l} e ()
  putStr : String -> App {l} e ()
  getChar : App {l} e Char
  getLine : App {l} e String

它提供了用于写入和读取控制台的原语，并将路径参数推广到 | 意味着两者都不能抛出异常，因为它们必须在 NoThrow 和 MayThrow 上下文中工作。

为了在顶层 IO 程序中实现这一点，我们需要访问原始的 IO 操作。 Control.App 库为此定义了一个原语接口：

interface PrimIO e where
  primIO : IO a -> App {l} e a
  fork : (forall e' . PrimIO e' => App {l} e' ()) -> App e ()

我们使用 primIO 来调用 IO 函数。我们还有一个 fork 原语，它在支持 PrimIO 的新错误列表中启动一个新线程。请注意， fork 启动了一个新的错误列表 e ，因此状态仅在单个线程中可用。

PrimIO 有一个错误列表的实现，可以将空类型作为异常抛出。这意味着如果 PrimIO 是唯一可用的接口，我们不能抛出异常，这与 IO 的定义是一致的。这也允许我们在初始错误列表 Init 中使用 PrimIO 。

HasErr AppHasIO e => PrimIO e where ...

鉴于此，我们可以实现 Console 并在 IO 中运行我们的 hello 程序。它在 Control.App.Console 中实现如下：

PrimIO e => Console e where
  putChar c = primIO $ putChar c
  putStr str = primIO $ putStr str
  getChar = primIO getChar
  getLine = primIO getLine

示例：文件 I/O

控制台 I/O 可以直接实现，但大多数 I/O 操作可能会失败。例如，打开文件失败的原因有多种：文件不存在；用户拥有错误的权限等。在 Idris 中， IO 原语在其类型中反映了这一点：

openFile : String -> Mode -> IO (Either FileError File)

虽然精确，但当有很长的 IO 操作序列时，这会变得笨拙。使用 App 时，我们可以提供一个接口，当操作失败时抛出异常，并保证使用 handle 在顶层处理任何异常。我们首先在 Control.App.FileIO 中定义 FileIO 接口：

interface Has [Exception IOError] e => FileIO e where
  withFile : String -> Mode ->
             (onError : IOError -> App e a) ->
             (onOpen : File -> App e a) ->
             App e a
  fGetStr : File -> App e String
  fGetChars : File -> Int -> App e String
  fGetChar : File -> App e Char
  fPutStr : File -> String -> App e ()
  fPutStrLn : File -> String -> App e ()
  fflush : File -> App e ()
  fEOF : File -> App e Bool

我们使用资源括号 - 将函数传递给 withFile 来处理打开的文件 - 而不是显式的 open 操作来打开文件，以确保文件句柄在完成时被清理。

还可以想象一个接口使用文件的线性资源，这在某些安全关键的上下文中可能是合适的，但对于大多数编程任务，异常应该就足够了。所有的操作都可能失败，接口明确表示，如果错误列表支持抛出和捕获 IOError 异常，我们只能实现 FileIO 。 IOError 在 Control.App 中定义。

例如，我们可以使用这个接口来实现 readFile ，如果在 withFile 中打开文件失败则抛出异常：

readFile : FileIO e => String -> App e String
readFile f = withFile f Read throw $ \h =>
               do content <- read [] h
                  pure (concat content)
where
  read : List String -> File -> App e (List String)
  read acc h = do eof <- fEOF h
                  if eof then pure (reverse acc)
                         else do str <- fGetStr h
                                 read (str :: acc) h

同样，这是在 Control.App.FileIO 中定义的。

要实现 FileIO ，我们需要通过 PrimIO 访问原始操作，以及在任何操作失败时抛出异常的能力。有了这个，我们可以如下实现 withFile ，例如：

Has [PrimIO, Exception IOError] e => FileIO e where
  withFile fname m onError proc
      = do Right h <- primIO $ openFile fname m
              | Left err => onError (FileErr (toFileEx err))
           res <- catch (proc h) onError
           primIO $ closeFile h
           pure res
  ...

鉴于 FileIO 的这个实现，我们可以运行 readFile ，前提是我们将它包装在一个顶级的 handle 函数中以处理 readFile 抛出的任何错误：

readMain : String -> App Init ()
readMain fname = handle (readFile fname)
       (\str => putStrLn $ "Success:\n" ++ show str)
       (\err : IOError => putStrLn $ "Error: " ++ show err)