ST 介绍：用状态来工作¶

Control.ST 库提供了在函数中创建、读取、写入和销毁状态，以及在函数类型中跟踪状态变化的功能。它基于资源（Resources）的概念，本质上就是可变变量和依赖类型。 STrans 会在函数运行时跟踪资源的变化：

STrans : (m : Type -> Type) ->
         (resultType : Type) ->
         (in_res : Resources) ->
         (out_res : resultType -> Resources) ->
         Type

类型为 STrans m resultType in_res out_res_fn 的值表示一系列可以操作状态的动作。其参数分别为：

m 表示一个底层的计算上下文（Computation Context），各种动作会在其中执行。通常，它是一个实现了 Monad 的泛型，但并非必须如此。具体来说，我们无需理解单子（Monad）就能高效地使用 ST！
resultType 表示这一系列动作会产生的值的类型。
in_res 表示一个在执行动作之前可用的资源列表。
out_res 表示一个在执行动作之后可用的资源列表，它随动作的结果而不同。

我们可以用 STrans 在函数的类型中描述状态转移系统（State Transition Systems）。我们会在之后定义资源（Resources），现在你可以先把它看做“现实世界的状态”的抽象表示。通过给定输入资源（in_res）和输出资源（out_res），我们可以描述允许函数执行的前提条件（Precondition）和描述了函数如何影响世界的所有状态的后置条件（Postcondition）。

本节以一些 STrans 函数的小例子开始，看看如何执行它们。我们还介绍了 ST，一个类型级的函数，它能让我们简明地描述带有状态的函数的状态转移。

对示例进行类型检查

对于本节和整个教程，你需要 import Control.ST 并通过向 idris 传递 -p contrib 参数来添加 contrib 包。

初试：操作 `State`¶

STrans 函数的类型解释了它如何影响一组 Resources。资源拥有一个类型为 Var 的标签（label），我们会用它在函数中引用该资源，并通过 label ::: type 的形式将该资源的状态写入``Resources`` 列表。

例如，以下函数的输入资源为 x，类型为 State Integer；输出资源的类型仍为 State Integer :

increment : (x : Var) -> STrans m () [x ::: State Integer]
                                     (const [x ::: State Integer])
increment x = do num <- read x
                 write x (num + 1)

本函数通过 read 读取资源 x 中存储的值，将其自增后的结果用 write 写回资源 x 中。稍后我们会看到 read 和 write 的类型（见 STrans 的原语操作）。我们还可以创建和删除资源：

makeAndIncrement : Integer -> STrans m Integer [] (const [])
makeAndIncrement init = do var <- new init
                           increment var
                           x <- read var
                           delete var
                           pure x

makeAndIncrement 的类型指明了它的入口（[]）和出口（const []）中没有可用的资源。它会用 new 创建一个新的 State 资源（接受一个资源的初始值），对其值自增，将该值读出来，然后用 delete 删除它，返回该资源的最终值。我们后面同样会看到 new 和 delete 的类型。

STrans``（类型为 ``Type -> Type）的参数 m 叫做计算上下文（Computation Context），函数会在其中运行。在这里，该类型级变量指明了我们可以在任何上下文中运行它。我们可以在同一个上下文中用 runPure 运行它。例如，将以上定义保存在 Intro.idr 文件中，然后在 REPL 中运行以下语句：

*Intro> runPure (makeAndIncrement 93)
94 : Integer

通过交互式的，类型驱动的方式来实现 STrans 是个不错的主意。例如，在通过 new init 创建了资源后，你可以为程序剩余的部分留一个坑（Hole）来看到资源的创建是如何影响类型的：

makeAndIncrement : Integer -> STrans m Integer [] (const [])
makeAndIncrement init = do var <- new init
                           ?whatNext

如果你检查一下 ?whatNext 的类型，就会发现有一个可用的资源 var，而在函数调用完成后应当不会再有可用的资源：

  init : Integer
  m : Type -> Type
  var : Var
--------------------------------------
whatNext : STrans m Integer [var ::: State Integer] (\value => [])

这个小例子可以在任何计算上下文 m 中工作。然而通常，我们会在一个更加严格的上下文中工作。例如，我们可能想要编写一个只能在支持交互式程序的上下文中工作的程序。为此，我们需要学习如何从底层上下文中提升（Lift）操作。

提升：使用计算上下文¶

比如说，我们现在并不想直接把初始整数传入 makeAndIncrement，而是想要把它从控制台读进来。那么我们就要把一般的工作上下文 m 换成特定的上下文 IO：

ioMakeAndIncrement : STrans IO () [] (const [])

lift 函数给了我们访问 IO 操作的方式。我们可以将 ioMakeAndIncrement 定义如下：

ioMakeAndIncrement : STrans IO () [] (const [])
ioMakeAndIncrement
   = do lift $ putStr "Enter a number: "
        init <- lift $ getLine
        var <- new (cast init)
        lift $ putStrLn ("var = " ++ show !(read var))
        increment var
        lift $ putStrLn ("var = " ++ show !(read var))
        delete var

lift 函数能让我们直接使用底层计算上下文（此处为 IO）中的函数。同样，我们很快就会看到 lift 具体的类型。

!-记法

在 ioMakeAndIncrement 中，我们使用了 !(read var) 从资源中读取信息。你可以在 Idris 教程（见单子与 do-记法）中找到关于 !-记法的详情。简单来说，它允许我们直接就地使用 STrans 类型的函数，而不必先将其结果绑定到一个变量。

至少从概念上来说，你可以将它当做拥有以下类型的函数：

(!) : STrans m a state_in state_out -> a

这个语法糖会在执行 do-语句块中的当前动作之前立即绑定一个变量，然后在 !-表达式的位置就地使用该变量。

然而在实践中，使用像 IO 这样特定的上下文通常是种糟糕的做法。首先，它需要我们在代码中到处泼洒 lift，这会影响可读性。再者，也是更重要的一点，它会降低函数的安全性，我们会在下一节（用类型表示状态机）中看到这一点。

所以我们改用定义接口的方式来限制计算上下文。例如，Control.ST 中定义了 ConsoleIO 接口，它为控制台的基本交互提供了必要的方法：

interface ConsoleIO (m : Type -> Type) where
  putStr : String -> STrans m () res (const res)
  getStr : STrans m String res (const res)

也就是说，我们能够以任何可用的资源 res 读写控制台，这两个方法均不会对可用的资源产生影响。IO 对它的实现如下：

ConsoleIO IO where
  putStr str = lift (Interactive.putStr str)
  getStr = lift Interactive.getLine

现在，我们可以将 ioMakeAndIncrement 定义为：

ioMakeAndIncrement : ConsoleIO io => STrans io () [] (const [])
ioMakeAndIncrement
   = do putStr "Enter a number: "
        init <- getStr
        var <- new (cast init)
        putStrLn ("var = " ++ show !(read var))
        increment var
        putStrLn ("var = " ++ show !(read var))
        delete var

它不仅可以在特定的 IO 中工作，还可以在一般的 io 上下文中工作，我们只需在该上下文中提供一个 ConsoleIO 的实现即可。相较于初版而言，它有以下优点：

所有对 lift 的调用都在接口的实现中，而非在 ioMakeAndIncrement 中
我们可以提供另一种 ConsoleIO 的实现，比如在基本的 I/O 中支持异常或日志。
在下一节（用类型表示状态机）中我们将会看到，它可以让我们定义安全的 API，以便更加精确地操作具体的资源。

我们之前在同一个上下文中使用 runPure 来运行 makeAndIncrement。而在这里，我们则使用 run，它能够让我们在任何上下文中执行 STrans 程序（只要该上下文实现了 Applicative 即可）。我们可以像下面这样在 REPL 中执行 ioMakeAndIncrement：

*Intro> :exec run ioMakeAndIncrement
Enter a number: 93
var = 93
var = 94

用依赖类型操作 `State`¶

在第一个 State 的例子中，当我们将值自增后，其类型并未改变。然而，当我们使用依赖类型时，状态的更新同样也会涉及到其类型的更新。例如，当我们向存储在状态中的向量添加一个元素时，其长度会改变：

addElement : (vec : Var) -> (item : a) ->
             STrans m () [vec ::: State (Vect n a)]
                  (const [vec ::: State (Vect (S n) a)])
addElement vec item = do xs <- read vec
                         write vec (item :: xs)

注意你需要 import Data.Vect 来执行此示例。

直接用 update 更新状态

除了分别使用 read 和 write 以外，你还可以使用 update，它从一个 State 中读取内容，对它应用一个函数，然后写入其结果。通过 update 你可以将 addElement 写为如下形式：

addElement : (vec : Var) -> (item : a) ->
             STrans m () [vec ::: State (Vect n a)]
                  (const [vec ::: State (Vect (S n) a)])
addElement vec item = update vec (item ::)

然而，我们并不总是能够知道在一系列动作中类型具体是如何变化的。例如，如果我们有一个包含整数向量的状态，那么可以从控制台读取一个输入，只有当该输入为有效的整数时才将它添加到该向量中。根据该整数是否读取成功，我们的输出状态会有不同的类型，简直令人无语。因此，下面两个函数的类型都不太正确：

readAndAdd_OK : ConsoleIO io => (vec : Var) ->
                STrans m ()  -- 返回空元组
                            [vec ::: State (Vect n Integer)]
                     (const [vec ::: State (Vect (S n) Integer)])
readAndAdd_Fail : ConsoleIO io => (vec : Var) ->
                  STrans m ()  -- 返回空元组
                              [vec ::: State (Vect n Integer)]
                       (const [vec ::: State (Vect n Integer)])

不过请记住，输出资源的类型可以从函数的结果中计算出来。目前，我们用 const 表示输出资源总是保持不变。不过在这里，我们可以用一个类型级函数来计算出输出资源。我们首先将返回空元组改为 Bool，当读取输入成功时它返回 True；然后为输出资源挖一个坑：

readAndAdd : ConsoleIO io => (vec : Var) ->
             STrans m Bool [vec ::: State (Vect n Integer)]
                           ?output_res

如果你检查 ?output_res 的类型，就会看到 Idris 期望一个类型为 Bool -> Resources 的函数，它表示输出资源的类型可以随 readAndAdd 的结果而不同：

  n : Nat
  m : Type -> Type
  io : Type -> Type
  constraint : ConsoleIO io
  vec : Var
--------------------------------------
output_res : Bool -> Resources

所以，当输入无效时，输出资源为 Vect n Integer（例如 readAndAdd 返回 False）；当输入有效时，输出资源为 Vect (S n) Integer。我们可以用类型将它表示出来：

readAndAdd : ConsoleIO io => (vec : Var) ->
             STrans io Bool [vec ::: State (Vect n Integer)]
                   (\res => [vec ::: State (if res then Vect (S n) Integer
                                                   else Vect n Integer)])

接着，我们在实现 readAndAdd 时需要为输出的状态返回适当的值。如果为向量添加了一个元素，就返回 True，否则就要返回 False：

readAndAdd : ConsoleIO io => (vec : Var) ->
             STrans io Bool [vec ::: State (Vect n Integer)]
                   (\res => [vec ::: State (if res then Vect (S n) Integer
                                                   else Vect n Integer)])
readAndAdd vec = do putStr "Enter a number: "
                    num <- getStr
                    if all isDigit (unpack num)
                       then do
                         update vec ((cast num) ::)
                         pure True     -- 添加一个元素，因此返回 True
                       else pure False -- 没有添加元素，因此返回 False

如果进行交互式开发的话则稍微有点不同。如果我们挖一个坑，那么在知道要返回的值以前，所需的输出状态并不显而易见。例如，在以下未完成的 readAndAdd 定义中，我们为成功的情况留了个坑：

readAndAdd vec = do putStr "Enter a number: "
                    num <- getStr
                    if all isDigit (unpack num)
                       then ?whatNow
                       else pure False

我们可以查看 ?whatNow 的类型，很遗憾信息不足：

  vec : Var
  n : Nat
  io : Type -> Type
  constraint : ConsoleIO io
  num : String
--------------------------------------
whatNow : STrans io Bool [vec ::: State (Vect (S n) Integer)]
                 (\res =>
                    [vec :::
                     State (ifThenElse res
                                       (Delay (Vect (S n) Integer))
                                       (Delay (Vect n Integer)))])

问题是我们只有在知道值会被返回时才能知道需要的输出状态。为了帮助交互式开发， Control.ST 提供了一个 returning 函数，我们可以用它来提前指定返回值，然后更新相应的状态。例如，我们可以将未完成的 readAndAdd 编写为：

readAndAdd vec = do putStr "Enter a number: "
                    num <- getStr
                    if all isDigit (unpack num)
                       then returning True ?whatNow
                       else pure False

它表示在成功的分支中，我们会返回 True，?whatNow 应该解释如何相应地更新状态，使其对于返回值 True 来说是正确的。我们只需检查 ?whatNow，就会发现现在的信息多了一点：

  vec : Var
  n : Nat
  io : Type -> Type
  constraint : ConsoleIO io
  num : String
--------------------------------------
whatnow : STrans io () [vec ::: State (Vect n Integer)]
                 (\value => [vec ::: State (Vect (S n) Integer)])

现在这个类型表示，在 STrans 的输出资源列表中，我们可以通过向 vec 添加一个元素来完成其定义：

readAndAdd vec = do putStr "Enter a number: "
                    num <- getStr
                    if all isDigit (unpack num)
                       then returning True (update vec ((cast num) ::))
                       else returning False (pure ()) -- 返回 False，因此无需更新状态

`STrans` 的原语操作¶

我们已经写过几个关于 STrans 函数的小例子了，是时候详细地了解这些状态操作函数了。首先，为了读写状态，我们使用了 read 和 write 函数：

read : (lbl : Var) -> {auto prf : InState lbl (State ty) res} ->
       STrans m ty res (const res)
write : (lbl : Var) -> {auto prf : InState lbl ty res} ->
        (val : ty') ->
        STrans m () res (const (updateRes res prf (State ty')))

它们的类型看起来有点吓人，特别是隐式的 prf 参数，其类型为：

prf : InState lbl (State ty) res

它依赖于一个断言 InState。一个类型为 InState x ty res 的值表示在资源列表 res 中，引用 x 的类型必须为 ty。实际上，所有这种类型都表示，如果一个对某资源的引用存在于资源列表中，那么我们我们只能读取或写入该资源。

给定一个资源标签 res 和一个 res 存在于资源列表中的证明，那么 updateRes 会更新该资源的类型。因此，write 的类型表示该资源的类型会被更新为给定值的类型。

update 的类型与 read 和 write 类型类似，它也需要资源的类型为给定函数的输入类型，并将它更新为该函数的输出类型：

update : (lbl : Var) -> {auto prf : InState lbl (State ty) res} ->
         (ty -> ty') ->
         STrans m () res (const (updateRes res prf (State ty')))

new 的类型表示它返回一个 Var，给定一个类型为 state 的初始值，输出资源包含一个新的类型为 State state 的资源：

new : (val : state) ->
      STrans m Var res (\lbl => (lbl ::: State state) :: res)

新资源的类型为 State state 而非只是 state 这一点很重要，因为这能让我们隐藏 API 的实现细节。在下一节用类型表示状态机中，我们会看到更多关于其意义的内容。

delete 的类型表示，给定一个标签存在于输入资源内的隐式证明，该标签会从资源列表中移除：

delete : (lbl : Var) -> {auto prf : InState lbl (State st) res} ->
         STrans m () res (const (drop res prf))

这里的 drop 是一个类型级函数，它用于更新资源列表，从该列表中移除给定的资源 lbl。

我们之前已经用 lift 在底层上下文中运行过函数了。它的类型如下：

lift : Monad m => m t -> STrans m t res (const res)

给定一个 result 值，pure 会返回产生该值的 STrans 程序，当产生该值时，它会假设当前资源列表是正确：

pure : (result : ty) -> STrans m ty (out_fn result) out_fn

我们可以用 returning 将从 STrans 函数中返回值的过程分为两部分：提供值本身，以及更新资源列表使其对应于该返回值：

returning : (result : ty) ->
            STrans m () res (const (out_fn result)) ->
            STrans m ty res out_fn

最后，我们已经用 run 和 runPure 在特定上下文中执行过 STrans 函数了。run 会在任何上下文中执行函数，若该上下文实现了 Applicative，那么 runPure 会在同一上下文中执行函数：

run : Applicative m => STrans m a [] (const []) -> m a
runPure : STrans Basics.id a [] (const []) -> a

注意在任何情况下，输入和输出资源列表都必须为空。没有一种方法能够提供初始资源列表，或提取最终的资源。这是有意设计的：它确保了所有的资源管理都在受控的 STrans 环境下进行，并且我们将会看到，这能够让我们实现安全的 API，以精确的类型来解释在程序的执行过程中，资源是如何被跟踪的。

这些函数构成了 ST 库的核心。在遇到更加复杂的情况时，我们还会用到一些其它的函数，不过目前所见的函数足以让我们用 Idris 进行细致的状态跟踪和推理了。

`ST`：直接表示状态转移¶

我们已经见过一些简单的 STrans 函数的例子了，由于需要提供显式的输入输出资源列表，它们的类型会变得非常冗长。在需要为原语操作提供类型时这很方便，不过对于更一般的使用来说，能为独立的资源表示状态转移，而无需完整地给出输入和输出资源列表的话会更加方便。我们可以用 ST 来做到这一点：

ST : (m : Type -> Type) ->
     (resultType : Type) ->
     List (Action resultType) -> Type

ST 是一个类型级函数，它会为给定的活动（Action）列表计算出对应的 STrans 类型，该类型描述了资源的状态转移。函数类型中的 Action 可接受以下形式（我们之后还会见到其它形式）：

lbl ::: ty 表示资源 lbl 的开始和结束状态均为 ty
lbl ::: ty_in :-> ty_out 表示资源 lbl 以状态 ty_in 开始，以状态 ty_out 结束
lbl ::: ty_in :-> (\res -> ty_out) 表示资源 lbl 以状态 ty_in 开始，以状态 ty_out 结束，其中 ty_out 从函数 res 的结果中计算而来。

现在，我们可以将前面的一些函数的类型写成如下形式：

increment : (x : Var) -> ST m () [x ::: State Integer]

即，increment 的开始和结束状态均为 State Integer 状态的 x。

makeAndIncrement : Integer -> ST m Integer []

即，makeAndIncrement 的开始和结束均没有资源。

addElement : (vec : Var) -> (item : a) ->
             ST m () [vec ::: State (Vect n a) :-> State (Vect (S n) a)]

即，addElement 将 vec 从 State (Vect n a) 改变为 State (Vect (S n) a)。

readAndAdd : ConsoleIO io => (vec : Var) ->
             ST io Bool
                   [vec ::: State (Vect n Integer) :->
                    \res => State (if res then Vect (S n) Integer
                                          else Vect n Integer)]

我们通过这种编写类型的方式，表达出了每个函数如何影响整体资源状态的最小必要条件。如果某个资源的更新依赖于某个结果（如 readAndAdd），那么我们需要完整地描述它。否则（如 increment 和 makeAndIncrement），我们可以写出输入输出资源列表以避免重复。

Action 也可以描述添加和移除状态：

add ty，如果该操作返回一个 Var，那么它会添加一个 ty 类型的新资源。
remove lbl ty 表示该操作会从资源列表中的状态 ty 开始，移除名为 lbl 的资源。

例如，我们可以写出：

newState : ST m Var [add (State Int)]
removeState : (lbl : Var) -> ST m () [remove lbl (State Int)]

第一个函数 newState 返回一个新的资源标签并将该资源添加到 State Int 类型的资源列表中。第二个函数 removeState 根据给定的标签 lbl 从列表中移除该资源。二者的类型与以下形式等价：

newState : STrans m Var [] (\lbl => [lbl ::: State Int])
removeState : (lbl : Var) -> STrans m () [lbl ::: State Int] (const [])

它们是构造 Action 的原语方法。我们后面还会遇到一些用类型级函数来提高可读性的方式。

除了极少数需要准确完整的 STrans 的情况外，在本教程剩余的部分中，我们通常会使用 ST。在下一节中，我们会看到如何用 ST 提供的设施来为需要安全性的系统编写准确的 API：一个需要登录的数据存储系统。

ST 介绍：用状态来工作¶

初试：操作 State¶

提升：使用计算上下文¶

用依赖类型操作 State¶

STrans 的原语操作¶

ST：直接表示状态转移¶

初试：操作 `State`¶

用依赖类型操作 `State`¶

`STrans` 的原语操作¶

`ST`：直接表示状态转移¶