复合状态机¶
在上一节中，我们定义了 DataStore 接口并用它实现了以下小程序，它能让用户登录该存储系统然后打印存储的内容：
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
该函数只用了一个状态，即存储本身。然而，更大的程序通常会有更多的状态，在执行过程中可能还需要添加、删除或更新状态。就本例而言，无限循环，在状态中记录登录失败的次数都是有用的扩展。
此外，状态机还可以有层级，即一个状态机可以通过复合其它状态机来实现。例如，我们可以有一个表示图形系统的状态机，并用它来实现「海龟绘图」这种高级的图形 API，「海龟绘图」会使用图形系统加上一些额外的状态。
在本节中，我们会看到如何使用多个状态工作，以及如何将状态机复合成更高级别的状态机。我们先来看看如何为 getData 添加登录失败的计数器。
使用多个资源来工作¶
为了了解如何使用多个资源来工作，我们需要修改 getData 使其循环，然后记录用户登录失败的总次数。例如，如果我们编写的 main 程序初始记录次数为 0，
那么会话过程看起来可能会是这样的：
*LoginCount> :exec main
Enter password: Mornington Crescent
Secret is: "Secret Data"
Enter password: Dollis Hill
Failure
Number of failures: 1
Enter password: Mornington Crescent
Secret is: "Secret Data"
Enter password: Codfanglers
Failure
Number of failures: 2
...
我们首先为 getData 添加一个跟踪失败次数的状态资源：
getData : (ConsoleIO m, DataStore m) =>
(failcount : Var) -> ST m () [failcount ::: State Integer]
getData 的类型检查
如果你跟着本教程写代码，就会发现更新了 getData 的类型后就无法通过编译了。这是意料之中的！我们暂且先将 getData 的定义注释掉，回头再说。
接着，我们创建一个 main 程序，它将状态初始化为 0，然后调用 getData：
main : IO ()
main = run (do fc <- new 0
getData fc
delete fc)
现在着手实现 getData。我们先来添加一个参数表示允许的失败次数：
getData : (ConsoleIO m, DataStore m) =>
(failcount : Var) -> ST m () [failcount ::: State Integer]
getData failcount
= do st <- connect
OK <- login st
| BadPassword => do putStrLn "Failure"
disconnect st
secret <- readSecret st
putStrLn ("Secret is: " ++ show secret)
logout st
disconnect st
然而，它无法通过类型检查，因为我们用来调用 connect 的资源不正确。错误信息描述了资源为何不必配：
When checking an application of function Control.ST.>>=:
Error in state transition:
Operation has preconditions: []
States here are: [failcount ::: State Integer]
Operation has postconditions: \result => [result ::: Store LoggedOut] ++ []
Required result states here are: st2_fn
换句话说，connect 需要在进入时没有资源，但我们却有一个资源，即失败次数！这理应没什么问题：毕竟我们需要的资源是拥有的资源的子集，而额外的资源（这里是失败次数）与 connect 无关。因此我们需要一种临时隐藏附加资源的方法。
我们可以用 call 函数来达此目的：
getData : (ConsoleIO m, DataStore m) =>
(failcount : Var) -> ST m () [failcount ::: State Integer]
getData failcount
= do st <- call connect
?whatNow
我们在这里为 getData 剩下的部分挖了个坑，这样你可以看到 call 的作用。它移除了调用 connect 时资源列表中不必要的部分，然后在返回时恢复了它们。因此 whatNow 的类型表明我们添加了一个新的资源 st，而 failcount依然可用：
failcount : Var
m : Type -> Type
constraint : ConsoleIO m
constraint1 : DataStore m
st : Var
--------------------------------------
whatNow : STrans m () [failcount ::: State Integer, st ::: Store LoggedOut]
(\result => [failcount ::: State Integer])
在此函数函数的最后，whatNow 表明我们需要以状态 st 结束，然而此时尚有
failcount 可用。我们可以在调用数据存储系统中的操作时添加 call
来消除资源列表，这样完成的 getData 就能带着附加的状态资源工作：
getData : (ConsoleIO m, DataStore m) =>
(failcount : Var) -> ST m () [failcount ::: State Integer]
getData failcount
= do st <- call connect
OK <- call $ login st
| BadPassword => do putStrLn "Failure"
call $ disconnect st
secret <- call $ readSecret st
putStrLn ("Secret is: " ++ show secret)
call $ logout st
call $ disconnect st
这样有点啰嗦，实际上我们可以将 call 变成隐式的从而去掉它。默认情况下，你需要显式地添加 call，但如果你导入了 Control.ST.ImplicitCall，那么
Idris 就会在需要的地方插入它。
import Control.ST.ImplicitCall
现在的 getData 就和之前一样了：
getData : (ConsoleIO m, DataStore m) =>
(failcount : Var) -> ST m () [failcount ::: State Integer]
getData failcount
= do st <- connect
OK <- login st
| BadPassword => do putStrLn "Failure"
disconnect st
secret <- readSecret st
putStrLn ("Secret is: " ++ show secret)
logout st
disconnect st
这里需要权衡：如果你导入了 Control.ST.ImplicitCall，那么使用多个资源的函数会更加易读，因为没有啰嗦的 call 了。另一方面，Idris 对你函数的类型检查会变得有点困难，这会导致它花费更多时间，错误信息也会少一点帮助。
看一下 call 的类型，你会有所启发：
call : STrans m t sub new_f -> {auto res_prf : SubRes sub old} ->
STrans m t old (\res => updateWith (new_f res) old res_prf)
被调用的函数有一个资源列表 sub，还有一个隐式证明 SubRes sub old，它证明了被调用函数的资源列表是整个资源列表的子集。尽管资源的顺序可以改变，然而在 old
中出现的资源无法在 sub 列表中出现超过一次（如果你尝试它就会得到一个类型错误）。
函数 updateWith 接受被调用函数的输出资源，然后在当前资源列表中更新它们。此函数会尽可能保持顺序不变，尽管被调用的函数在进行复杂的资源操作时并不总是可以保持顺序。
在被调用的函数中新创建的资源
如果被调用的函数创建了新的资源，那么基于 updateWith 的工作方式，它们通常会出现在资源列表的末尾。你可以在前面未完成的 getData
的定义中看到这一点。
最后我们可以更新 getData 使其可以循环，并在需要时保持更新 failCount：
getData : (ConsoleIO m, DataStore m) =>
(failcount : Var) -> ST m () [failcount ::: State Integer]
getData failcount
= do st <- call connect
OK <- login st
| BadPassword => do putStrLn "Failure"
fc <- read failcount
write failcount (fc + 1)
putStrLn ("Number of failures: " ++ show (fc + 1))
disconnect st
getData failcount
secret <- readSecret st
putStrLn ("Secret is: " ++ show secret)
logout st
disconnect st
getData failcount
注意在这里我们会在每次迭代中建立并断开连接。另一种实现方式是首先用 connect
建立连接，然后调用 getData，其实现如下：
getData : (ConsoleIO m, DataStore m) =>
(st, failcount : Var) -> ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
getData st failcount
= do OK <- login st
| BadPassword => do putStrLn "Failure"
fc <- read failcount
write failcount (fc + 1)
putStrLn ("Number of failures: " ++ show (fc + 1))
getData st failcount
secret <- readSecret st
putStrLn ("Secret is: " ++ show secret)
logout st
getData st failcount
在 st 的类型 Store {m} LoggedOut 中添加显式的 {m} 是十分重要的，因为这给了
Idris 足够的信息来判断哪一个 DataStore 的实现是用于查找其对应的 Store 的实现的。
否则，如果我们只写 Store LoggedOut，那么将无法获知 Store 所关联到的计算上下文 m。
接着我们可以在 main 中只 connect 并 disconnect 一次：
main : IO ()
main = run (do fc <- new 0
st <- connect
getData st fc
disconnect st
delete fc)
通过使用 call 或导入 Control.ST.ImplicitCall，我们可以编写使用多个资源的程序，
然后在调用一个只用到全部资源的子集的函数时，将资源列表按需删减。
复合资源：状态机的层级¶
我们现在已经见过如何在一个函数中使用多个资源了，这对于任何能够操作状态的实际的程序来说都是必须的。我们可以把它看做是「横向的」复合：一次使用多个资源。我们通常还需要「纵向」的复合：基于一个或多个资源来实现单个资源。
在本节中，我们会看到一个这种的例子。首先，我们在一个接口 Draw
中实现一个小型的图形 API，它支持：
- 打开一个窗口，创建一个双缓冲（double-buffered）的平面（surface）来绘图
- 在平面上绘制线条和矩形
- 缓冲区「翻页（flipping）」，在窗口中显示我们刚绘制完毕的图像
- 关闭一个窗口
提示
绘图并不是即时呈现的，需要一个缓冲区（buffer）来暂存即将呈现的图像。 缓冲区一般有三个基本操作：clear（清空），flip（翻页）和 rewind（重显）。 clear 会将当前缓冲区清空以便重新绘图；flip 会将当前缓冲区中的图像显示在屏幕上，然后清空缓冲区等待下一次绘图；而 rewind 则保持缓冲区内容不变，重新显示到屏幕上。
术语 flip 和 rewind 来源于磁带的播放，rewind 即倒带重放，而 flip 则表示把磁带翻过来播放另一面。flip 一词尚无标准译法，此处译作「翻页」表示本画面完成，开始下一画面。
接着，我们在一个 interface 中用此 API 来为「海龟绘图」实现一个更高级的 API。这不仅需要 Draw 接口，还需要表示海龟的状态（位置，方向和画笔颜色）。
SDL 绑定
为了测试本节中的示例，你需要为 Idris 安装一个非常基本的 SDL 绑定，它可从 https://github.com/edwinb/SDL-idris 获取。这些绑定实现了 SDL API 的一个很小的子集，只用作演示的目的。尽管如此，它们已经足以实现一个小型的绘图程序来展示本节的概念了。
一旦你安装完这个包，就可以通过参数启动 Idris 了，-p sdl 用于 SDL 绑定，-p contrib 用于 Control.ST。
Draw 接口¶
我们要在此 API 中使用 Idris 的 SDL 绑定，因此你需要在安装完该绑定库后导入
Graphics.SDL。我们先来定义 Draw 接口，它包含一个表示平面的数据类型，我们会在其之上绘制线条和矩形：
interface Draw (m : Type -> Type) where
Surface : Type
我们需要能够通过打开新窗口来创建新的 Surface：
initWindow : Int -> Int -> ST m Var [add Surface]
然而这样不太正确。如果我们的程序运行在没有可用的窗口系统的终端环境中，那么打开窗口可能会失败。因此， initWindow 需要以某种方式来应对可能的失败。我们可以通过返回 Maybe Var 而非 Var，以及只在成功时添加 Surface
来做到这一点：
initWindow : Int -> Int -> ST m (Maybe Var) [addIfJust Surface]
它使用了 Control.ST 中定义的类型级函数 addIfJust，该函数返回一个
Action，仅在操作成功时添加资源（也就是说，它返回一个形如 Just val 的结果）。
addIfJust 与 addIfRight
Control.ST 中定义了能够在操作成功时构造新资源的函数，其中的 addIfJust
会在操作返回 Just ty 时添加资源。此外还有 addIfRight：
addIfJust : Type -> Action (Maybe Var)
addIfRight : Type -> Action (Either a Var)
二者均基于下面的原语动作 Add 开发。此动作接受一个函数，该函数从操作的结果中构造出一个资源列表：
Add : (ty -> Resources) -> Action ty
如有需要，你可以用它来创建自己的动作，以此来基于某个操作的结果添加资源。例如，addIfJust 的实现如下：
addIfJust : Type -> Action (Maybe Var)
addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
如果我们能创建窗口，那么也需要能删除它：
closeWindow : (win : Var) -> ST m () [remove win Surface]
我们还需要响应按下键盘或点击鼠标这类事件。Graphics.SDL 库为此提供了
Event 类型，而我们可以用 poll 轮询事件，如果存在的话，它会返回最后一个发生的事件：
poll : ST m (Maybe Event) []
Draw 中剩下的方法包括：flip，它会将从上次 flip 以来绘制的所有图像都显示出来；还有两个绘图的方法 filledRectangle 和 drawLine。
flip : (win : Var) -> ST m () [win ::: Surface]
filledRectangle : (win : Var) -> (Int, Int) -> (Int, Int) -> Col -> ST m () [win ::: Surface]
drawLine : (win : Var) -> (Int, Int) -> (Int, Int) -> Col -> ST m () [win ::: Surface]
我们按如下方式定义色彩，四个整数表示色彩通道（红、绿、蓝、不透明度）：
data Col = MkCol Int Int Int Int
black : Col
black = MkCol 0 0 0 255
red : Col
red = MkCol 255 0 0 255
green : Col
green = MkCol 0 255 0 255
-- 蓝、黄、品红、青、白类似……
在导入 Graphics.SDL 之后，你就可以像下面这样用 SDL 的绑定实现 Draw 接口了：
implementation Draw IO where
Surface = State SDLSurface
initWindow x y = do Just srf <- lift (startSDL x y)
| pure Nothing
var <- new srf
pure (Just var)
closeWindow win = do lift endSDL
delete win
flip win = do srf <- read win
lift (flipBuffers srf)
poll = lift pollEvent
filledRectangle win (x, y) (ex, ey) (MkCol r g b a)
= do srf <- read win
lift $ filledRect srf x y ex ey r g b a
drawLine win (x, y) (ex, ey) (MkCol r g b a)
= do srf <- read win
lift $ drawLine srf x y ex ey r g b a
在本实现中，我们使用 startSDL 来初始化窗口，它在失败时返回 Nothing。由于 initWindow 的类型说明它会在返回形如 Just val 的值时添加一个资源，
因此我们在成功时添加 startSDL 返回的平面，在失败时什么也不做。我们只能在
startDSL 成功时初始化成功。
现在我们有了 Draw 的实现，可以试着写一些函数了，他们在窗口中绘图并通过
SDL 绑定执行它们。例如，假设我们有一个可以绘图的平面 win，那么可以编写
render 函数在黑色背景上绘图：
render : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]
render win = do filledRectangle win (0,0) (640,480) black
drawLine win (100,100) (200,200) red
flip win
最后的 flip win 是必须的，因为绘图原语使用了双缓冲区来避免图形闪烁。我们在屏幕之外的缓冲区上绘图，同时显示另一个缓冲区。在调用 flip 时，它会将当前屏幕之外的缓冲区显示出来，并创建一个新的屏幕外缓冲区绘制下一帧。
要将它包含在程序里，我们需要编写一个主循环来渲染图像，同时等待用户关闭应用的事件：
loop : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]
loop win = do render win
Just AppQuit <- poll
| _ => loop win
pure ()
最后，我们创建一个主程序。如果可能，它会创建窗口，然后运行主循环：
drawMain : (ConsoleIO m, Draw m) => ST m () []
drawMain = do Just win <- initWindow 640 480
| Nothing => putStrLn "Can't open window"
loop win
closeWindow win
我们可以在 REPL 中用 run 运行它：
*Draw> :exec run drawMain
更高级的接口：TurtleGraphics¶
「海龟绘图」会操纵一只「海龟」在屏幕上移动，在它移动时用「画笔」来画线。一只海龟拥有描述它位置的属性，它面对的方向，以及当前画笔的颜色。此外，还有一些命令来让海龟向前移动，转一个角度，以及更改画笔的颜色。下面是一种可行的接口：
interface TurtleGraphics (m : Type -> Type) where
Turtle : Type
start : Int -> Int -> ST m (Maybe Var) [addIfJust Turtle]
end : (t : Var) -> ST m () [Remove t Turtle]
fd : (t : Var) -> Int -> ST m () [t ::: Turtle]
rt : (t : Var) -> Int -> ST m () [t ::: Turtle]
penup : (t : Var) -> ST m () [t ::: Turtle]
pendown : (t : Var) -> ST m () [t ::: Turtle]
col : (t : Var) -> Col -> ST m () [t ::: Turtle]
render : (t : Var) -> ST m () [t ::: Turtle]
和 Draw 一样，我们也需要一个初始化海龟的命令（这里叫做 start），如果它无法创建用来绘图的平面就会失败。此外还有一个 render 方法，它用来渲染窗口中目前已绘制的图像。使用此接口的一个可用的程序如下所示，它画了一个彩色的正方形：
turtle : (ConsoleIO m, TurtleGraphics m) => ST m () []
turtle = with ST do
Just t <- start 640 480
| Nothing => putStr "Can't make turtle\n"
col t yellow
fd t 100; rt t 90
col t green
fd t 100; rt t 90
col t red
fd t 100; rt t 90
col t blue
fd t 100; rt t 90
render t
end t
with ST do
在 turtle 中使用 with ST do 是为了区分 (>>=) 的版本，它可能来自于
Monad 或者 ST。虽然 Idris 自己能够解决此问题，不过它会尝试所有可能性，因此使用 with 从句可以减少耗时，加速类型检查。
要实现此接口，我们可以尝试用 Surface 来表示海龟用来作画的平面：
implementation Draw m => TurtleGraphics m where
Turtle = Surface {m}
知道了 Turtle 被表示为 Surface 之后，我们就能使用 Draw 提供的方法来实现海龟了。然而这还不够，我们还需要存储更多信息：具体来说，海龟有一些属性需要存储在某处。因此我们不仅需要将海龟表示为一个 Surface，还需要存储一些附加的状态。我们可以通过复合资源来做到这一点。
复合资源简介¶
复合资源由一个资源列表构造而来，它使用以下 Control.ST 中定义的类型实现：
data Composite : List Type -> Type
如果我们有一个复合资源，那么可以用 split 将其分解为构成它的资源，并为每个资源创建新的变量。例如：
splitComp : (comp : Var) -> ST m () [comp ::: Composite [State Int, State String]]
splitComp comp = do [int, str] <- split comp
?whatNow
调用 split comp 会从复合资源 comp 中提取出 State Int 和
State String，并分别将它们存储在变量 int 和 str 中。如果我们检查
whatNow 的类型，就会看到它影响了资源列表：
int : Var
str : Var
comp : Var
m : Type -> Type
--------------------------------------
whatNow : STrans m () [int ::: State Int, str ::: State String, comp ::: State ()]
(\result => [comp ::: Composite [State Int, State String]])
这样，我们就有了两个新的资源 int 和 str，而 comp 的类型则被更新为单元类型，
即当前没有保存数据。这点符合预期：我们只是要将数据提取为独立的资源而已。
现在我们提取出了独立的资源，可以直接操作它们（比如，增加 Int 或为 String
添加换行）并使用 combine 重新构造复合资源：
splitComp : (comp : Var) ->
ST m () [comp ::: Composite [State Int, State String]]
splitComp comp = do [int, str] <- split comp
update int (+ 1)
update str (++ "\n")
combine comp [int, str]
?whatNow
同样，我们可以检查 whatNow 的类型来查看 combine 的作用：
comp : Var
int : Var
str : Var
m : Type -> Type
--------------------------------------
whatNow : STrans m () [comp ::: Composite [State Int, State String]]
(\result => [comp ::: Composite [State Int, State String]])
所以 combine 的作用就是接受既有的资源并将它们合并成一个复合资源。在执行 combine 之前，目标资源必须存在（这里是 comp）且类型为 State ()。
查看 split 和 combine 的类型，了解它们使用的资源列表的要求是很有启发的。split 的类型如下：
split : (lbl : Var) -> {auto prf : InState lbl (Composite vars) res} ->
STrans m (VarList vars) res (\vs => mkRes vs ++ updateRes res prf (State ()))
隐式的 prf 参数说明要被分解的 lbl 必须为复合资源。它返回一个由复合资源分解而来的变量列表，而 mkRes 函数则创建一个对应类型的资源列表。最后，updateRes
会将复合资源的类型更新为 State ()。
而 combine 函数则反过来：
combine : (comp : Var) -> (vs : List Var) ->
{auto prf : InState comp (State ()) res} ->
{auto var_prf : VarsIn (comp :: vs) res} ->
STrans m () res (const (combineVarsIn res var_prf))
隐式的 prf 参数确保了目标资源 comp 的类型为 State ()。也就是说，我们不会覆盖任何其它的信息。隐式的 var_prf 参数类似于 call 中的 SubRes，它确保了我们用来构造复合资源的每个变量都确实存在于当前的资源列表中。
我们可以基于 Draw 以及任何需要的附加资源，通过复合资源的方式来实现高级的
TurtleGraphics API。
实现 Turtle¶
现在我们已经知道如何用一组既有的资源来构造出新的资源了。我们可以用复合资源实现
Turtle，它包括一个用于绘图的 Surface，以及一些表示画笔颜色、位置和方向的独立的状态。我们还有一个线条的列表，它描述了我们在调用 render 时要绘制到
Surface 上的图像：
Turtle = Composite [Surface {m}, -- 用来绘图的平面
State Col, -- 画笔颜色
State (Int, Int, Int, Bool), -- 画笔的位置/方向/落笔标记
State (List Line)] -- 渲染时要画的线条
一条 Line 由它的起始位置，终止位置和颜色定义：
Line : Type
Line = ((Int, Int), (Int, Int), Col)
首先来实现 start，它会创建一个新的 Turtle``（如果不可能则返回 ``Nothing）。我们从初始化绘图平面开始，然后是所有状态构成的组件。最后，我们将所有的组件组合成一个复合资源来表示海龟：
start x y = do Just srf <- initWindow x y
| Nothing => pure Nothing
col <- new white
pos <- new (320, 200, 0, True)
lines <- new []
turtle <- new ()
combine turtle [srf, col, pos, lines]
pure (Just turtle)
然后来实现 end，它会把海龟处理掉。我们先析构复合资源，然后关闭窗口，删除所有独立的资源。记住我们只能用 delete 删除一个 State，因此需要用 split
将复合资源分解掉，用 closeWindow 干净地关闭绘图平面，然后用 delete 删除状态：
end t = do [srf, col, pos, lines] <- split t
closeWindow srf; delete col; delete pos; delete lines; delete t
对于其它的方法，我们需要用 split 分解资源以获取每一个组件，然后在结束时用
combine 将它们组合成一个复合资源。例如，以下为 penup 的实现：
penup t = do [srf, col, pos, lines] <- split t -- 分解复合资源
(x, y, d, _) <- read pos -- 析构画笔位置
write pos (x, y, d, False) -- 将落笔标记置为 False
combine t [srf, col, pos, lines] -- 重新组合组件
海龟剩下的操作遵循相同的模式。完整的细节见 Idris 发行版中的
samples/ST/Graphics/Turtle.idr 文件。之后就是是渲染海龟创建的图像：
render t = do [srf, col, pos, lines] <- split t -- 分解复合资源
filledRectangle srf (0, 0) (640, 480) black -- 绘制背景
drawAll srf !(read lines) -- 渲染海龟绘制的线条
flip srf -- 缓冲区翻页以显示图像
combine t [srf, col, pos, lines]
Just ev <- poll
| Nothing => render t -- 继续直到按下按键
case ev of
KeyUp _ => pure () -- 按键按下，于是退出
_ => render t
where drawAll : (srf : Var) -> List Line -> ST m () [srf ::: Surface {m}]
drawAll srf [] = pure ()
drawAll srf ((start, end, col) :: xs)
= do drawLine srf start end col -- 按相应的颜色绘制线条
drawAll srf xs