用类型表示状态机¶
在概览一节中，我们用状态转移图展示了数据存储系统的抽象状态， 以及可以对它执行的动作：
我们之所以把它称作该存储系统的抽象状态，是因为具体的状态会包含更多信息。例如，它可能包含用户名、散列化的密码和存储内容等等。然而，就目前我们我们所关心的动作
login、logout 和 readSecret 而言，登录状态决定了哪些动作是有效的。
我们已经见过如何用 ST 操作状态，用依赖类型表示状态了。在本节中，我们会看到如何用
ST 为数据存储系统提供安全的 API。在 API 中，我们会用类型编码上面的状态转移图。
通过这种方式，我们可以只在状态有效时才能执行 login、logout 和 readSecret
操作。
我们已经用过 State 及其原语操作 new、read、write 和 delete
来操作状态了。而对于数据存储的 API，我们则以定义接口开始（见 Idris 教程中的接口一节）。接口描述了对存储系统的操作，其类型则准确解释了每种操作何时才有效，以及它是如何影响存储系统的状态的。通过接口，我们可以确保这是访问存储系统的唯一的方式。
为数据存储系统定义接口¶
我们首先在 Login.idr 文件中定义数据类型，它表示存储系统的两种抽象状态，即
LoggedOut 和 LoggedIn：
data Access = LoggedOut | LoggedIn
我们可以定义一个数据类型来表示存储系统的当前状态，保存所有必要的信息（如用户名、散列化的密码、存储内容等等），并根据登录状态来参数化该数据类型：
Store : Access -> Type
不过我们现在先不定义具体的类型，而是将以下代码包含在数据存储的接口中，之后再定义具体的类型：
interface DataStore (m : Type -> Type) where
Store : Access -> Type
我们可以继续为此接口补充其它存储系统的操作。这样做优点众多。通过将接口与其实现相分离，我们可以为不同的上下文提供相应的具体实现。此外，我们还可以编写与存储系统协作的程序而无需知道任何实现的细节。
我们需要用 connect 连接到该存储系统，在结束后用 disconnect 断开连接。
我们为 DataStore 接口添加以下方法：
connect : ST m Var [add (Store LoggedOut)]
disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
connect 的类型表明它会返回一个初始类型为 Store LoggedOut 的新资源。
反之，disconnect 则会给出一个状态为 Store LoggedOut 的资源并移除该资源。
我们可以通过以下（未完成的）定义更加清楚地看到 connect 做了什么：
doConnect : DataStore m => ST m () []
doConnect = do st <- connect
?whatNow
注意我们正在一个 一般的上下文 m 中工作，为了能够执行 doConnect，我们必须为 m 实现 DataStore 接口来限制它。如果我们检查 ?whatNow
的类型，就会看到剩下的操作以一个状态为 Store LoggedOut 的资源 st 开始，
以没有可用的资源结束：
m : Type -> Type
constraint : DataStore m
st : Var
--------------------------------------
whatNow : STrans m () [st ::: Store LoggedOut] (\result => [])
接着，我们可以用 disconnect 来移除该资源：
doConnect : DataStore m => ST m () []
doConnect = do st <- connect
disconnect st
?whatNow
现在检查 ?whatNow 的类型会显示我们没有可用的资源：
m : Type -> Type
constraint : DataStore m
st : Var
--------------------------------------
whatNow : STrans m () [] (\result => [])
为了继续完善 DataStore 接口的实现，我们接下来添加一个读取机密数据的方法。
这需要 store 的状态为 Store LoggedIn：
readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
此时我们可以试着编写一个函数，它先连接到存储系统，然后读取机密数据，之后断开连接。
然而它并不会成功，因为执行 readSecret 需要我们处于已登录状态。
badGet : DataStore m => ST m () []
badGet = do st <- connect
secret <- readSecret st
disconnect st
它会产生以下错误，因为 connect 创建了状态为 LoggedOut 的新存储，而
readSecret 需要该存储的状态为 LoggedIn：
When checking an application of function Control.ST.>>=:
Error in state transition:
Operation has preconditions: [st ::: Store LoggedOut]
States here are: [st ::: Store LoggedIn]
Operation has postconditions: \result => []
Required result states here are: \result => []
该错误信息解释了所需的输入状态（前提条件）和输出状态（后置条件）与该操作中的状态有何不同。为了使用 readSecret，我们需要一种方式将 Store LoggedOut 转换为
Store LoggedIn 状态。我们可以先尝试将 login（登录）指定为以下类型：
login : (store : Var) -> ST m () [store ::: Store LoggedOut :-> Store LoggedIn] -- 类型不正确！
注意，接口中并没有说明 login 是如何工作的，只是表达了它如何影响所有的状态。即便如此，login 的类型还是有点问题，因为它假设了登录总会成功。如果登录失败（比如在该实现提示输入密码时用户输入了错误的密码），那么它一定不会产生 LoggedIn 状态的存储。
因此，login 需要通过以下类型返回登录是否成功：
data LoginResult = OK | BadPassword
接着，我们可以从结果中计算出结果状态（见用依赖类型操作 State）。我们为
DataStore 接口添加以下方法：
login : (store : Var) ->
ST m LoginResult [store ::: Store LoggedOut :->
(\res => Store (case res of
OK => LoggedIn
BadPassword => LoggedOut))]
如果 login 成功，那么 login 之后的状态会变成 Store LoggedIn。否则，状态仍然为 Store LoggedOut。
为完成此接口，我们还需要添加一个退出该存储系统的方法。我们假设退出总是成功，并将存储系统的状态从 Store LoggedIn 转换为 Store LoggedOut。
logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
这样就完成了此接口。完整代码如下：
interface DataStore (m : Type -> Type) where
Store : Access -> Type
connect : ST m Var [add (Store LoggedOut)]
disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
login : (store : Var) ->
ST m LoginResult [store ::: Store LoggedOut :->
(\res => Store (case res of
OK => LoggedIn
BadPassword => LoggedOut))]
logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
在尝试创建此接口的实现之前，我们来看看如何用它来编写函数，以此来登录数据存储系统、在登录成功后读取机密数据，然后再退出。
用数据存储接口编写函数¶
我们以编写 getData 函数为例，展示如何使用 DataStore 接口。
该函数用于连接到存储系统并从中读取数据。我们使用该操作的类型来逐步指导开发，
交互式地编写此函数。它的类型如下：
getData : (ConsoleIO m, DataStore m) => ST m () []
该类型表示在进入或退出时没有资源可用。也就是说，整个动作列表为 []，这表示至少从外部来说，该函数完全没有对资源产生作用。换句话说，对于每一个在调用
getData 时创建的资源，我们都需要在退出前删除它。
由于我们要使用 DataStore 接口的方法，因此必须约束计算上下文 m
使其实现 DataStore 接口。我们还有一个 ConsoleIO m 约束，这样就能将我们从存储系统中读取的任何数据或者错误信息显示出来。
我们从连接到存储系统开始，创建一个新的资源 st，然后尝试用 login 登录：
getData : (ConsoleIO m, DataStore m) => ST m () []
getData = do st <- connect
ok <- login st
?whatNow
登录可能成功也可能失败，两种状态可从 ok 值反映出来。如果我们检查 ?whatNow
的类型，就会看到当前存储系统的状态：
m : Type -> Type
constraint : ConsoleIO m
constraint1 : DataStore m
st : Var
ok : LoginResult
--------------------------------------
whatNow : STrans m () [st ::: Store (case ok of
OK => LoggedIn
BadPassword => LoggedOut)]
(\result => [])
由于 st 的当前状态依赖于 ok 的值，因此我们可以对 ok 分情况讨论来继续推进：
getData : (ConsoleIO m, DataStore m) => ST m () []
getData = do st <- connect
ok <- login st
case ok of
OK => ?whatNow_1
BadPassword => ?whatNow_2
两个分支上的坑 ?whatNow_1 和 ?whatNow_2 的类型展现了状态是如何随着登录成功与否而改变的。如果登录成功，那么该存储系统的状态为 LoggedIn:
--------------------------------------
whatNow_1 : STrans m () [st ::: Store LoggedIn] (\result => [])
如果失败，那么它的状态为 LoggedOut:
--------------------------------------
whatNow_2 : STrans m () [st ::: Store LoggedOut] (\result => [])
在 ?whatNow_1 中，由于登录成功，因此可以读取机密数据并将它显示在终端上：
getData : (ConsoleIO m, DataStore m) => ST m () []
getData = do st <- connect
ok <- login st
case ok of
OK => do secret <- readSecret st
putStrLn ("Secret is: " ++ show secret)
?whatNow_1
BadPassword => ?whatNow_2
我们要以「无资源可用」的状态来结束 OK 分支，因此需要退出存储系统并断开连接：
getData : (ConsoleIO m, DataStore m) => ST m () []
getData = do st <- connect
ok <- login st
case ok of
OK => do secret <- readSecret st
putStrLn ("Secret is: " ++ show secret)
logout st
disconnect st
BadPassword => ?whatNow_2
注意我们在调用 disconnect 断开连接前，必须用 logout 退出
st，因为 disconnect 需要存储系统处于 LoggedOut 状态。
此外，我们不能像上一节中 State 的示例那样，简单地用 delete 来删除该资源，因为对于某个类型 ty 来说，delete 只能在资源的类型为 State ty 时起效。如果我们试图用 delete 来代替 disconnect，就会看到以下错误：
When checking argument prf to function Control.ST.delete:
Can't find a value of type
InState st (State st) [st ::: Store LoggedOut]
换句话说，类型检查器找不到一个「资源 st 拥有 State st 形式的类型」的证明，因为其类型为 Store LoggedOut。由于 Store 是 DataStore 接口的一部分，而我们尚未知道 Store 的具体表示，因此我们需要通过此接口的 disconnect
而非直接用 delete 来删除资源。
我们可以将 getData 完成如下，使用模式匹配来绑定候选（见 Idris 教程的单子与 do-记法），而非使用 case 语句来捕获 login 可能产生的错误：
getData : (ConsoleIO m, DataStore m) => ST m () []
getData = do st <- connect
OK <- login st
| BadPassword => do putStrLn "Failure"
disconnect st
secret <- readSecret st
putStrLn ("Secret is: " ++ show secret)
logout st
disconnect st
然而它现在还跑不起来，因为我们还没有任何 DataStore 的实现！如果我们试着在一个
IO 上下文中执行它，就会产生一个没有 DataStore IO 的实现的错误：
*Login> :exec run {m = IO} getData
When checking an application of function Control.ST.run:
Can't find implementation for DataStore IO
因此，要实现遵循其状态转移图的数据存储系统，最后一步就是提供一个 DataStore
的实现。
实现接口¶
要在 IO 中执行 getData，我们需要提供一个能够在 IO 上下文中工作的
DataStore 的实现。我们可以这样开始：
implementation DataStore IO where
接着，我们可以让 Idris 根据必要方法的基本定义来填充该接口（在 Atom 中按下
Ctrl-Alt-A，或者在你喜欢的编辑器中按下对应的快捷键来「添加定义」）：
implementation DataStore IO where
Store x = ?DataStore_rhs_1
connect = ?DataStore_rhs_2
disconnect store = ?DataStore_rhs_3
readSecret store = ?DataStore_rhs_4
login store = ?DataStore_rhs_5
logout store = ?DataStore_rhs_6
我们首先要确定表示该数据存储系统的方式。为简单起见，我们将数据存储为单个的
String，并使用硬编码的密码来获取访问权限。我们可以将 Store 定义如下，无论在 LoggedOut 还是在 LoggedIn 状态下均使用 String 来表示数据。
Store x = State String
现在我们给出了 Store 的一个具体类型，我们可以实现建立连接、断开连接和访问数据的操作。而由于我们使用了 State，因此也就可以使用 new、delete、read 和 write
来操作该存储系统。
坑的类型会告诉我们如何操作状态。例如，?DataStore_rhs_2 坑告诉我们要实现
connect 需要做些什么。我们需要返回一个新的 Var，表示一个类型为
State String 的资源：
--------------------------------------
DataStore_rhs_2 : STrans IO Var [] (\result => [result ::: State String])
我们可以通过创建一个带有某些数据作为存储内容的新变量来实现它（我们可以使用任何
String），然后返回该变量：
connect = do store <- new "Secret Data"
pure store
对于 disconnect 而言，我们只需删除该资源即可：
disconnect store = delete store
对于 readSecret，我们需要读取机密数据并返回 String。由于我们并不知道该数据的具体表示为 State String，因此可以直接用 read
来访问数据：
readSecret store = read store
我们先来完成 logout，之后回到 login 上来。检查坑的类型会显示以下信息：
store : Var
--------------------------------------
DataStore_rhs_6 : STrans IO () [store ::: State String] (\result => [store ::: State String])
因此在此小型实现中，我们实际上不用做任何事情！
logout store = pure ()
对于 login，我们需要返回登录是否成功。为此，我们需要提示用户输入密码，并在匹配到硬编码的密码时返回 OK，否则返回 BadPassword：
login store = do putStr "Enter password: "
p <- getStr
if p == "Mornington Crescent"
then pure OK
else pure BadPassword
下面给出完整的实现以供参考，它能让我们在 REPL 中执行 DataStore 程序：
implementation DataStore IO where
Store x = State String
connect = do store <- new "Secret Data"
pure store
disconnect store = delete store
readSecret store = read store
login store = do putStr "Enter password: "
p <- getStr
if p == "Mornington Crescent"
then pure OK
else pure BadPassword
logout store = pure ()
最后，我们可以像下面这样在 REPL 中尝试它（如果有可用的 IO 实现，那么在 Idris
的 REPL 中，上下文会默认为 IO，因此这里无需显式给出 m 参数）：
*Login> :exec run getData
Enter password: Mornington Crescent
Secret is: "Secret Data"
*Login> :exec run getData
Enter password: Dollis Hill
Failure
对于 State 类型的资源，我们只能使用 read、write、new 和 delete。因此，在 DataStore 的实现或任何已知上下文为 IO 的环境内部，我们可以随意访问数据存储系统，因为这里是实现 DataStore 内部细节的地方。然而，如果我们只有 DataStore m 的约束，那么就无法知道该存储系统是否已实现，因此我们只能通过 DataStore 提供的 API 来访问它。
因此比较好的做法是在 getData 这类函数中使用泛型（Generic）上下文 m，并只根据我们需要的接口进行约束，而非使用具体的上下文 IO。
现在我们已经学过如何处理状态，以及如何用接口来封装数据存储这类具体系统的状态转移了。 然而，真正的系统需要能够复合多种状态机。我们一次需要使用多个状态机，或者基于多个状态机来实现一个状态机。