Post #16

函数式编程中有一个概念叫 state monad，它将所有数据用形如 λs1.(s2,a) 的函数来表示，其中 s1 是某种旧状态，s2 是新状态，a 是计算结果。一个普通的数字 3 被表示为 λs.(s,3)，加法运算则可以定义为让两个参数中包含的状态变化依次发生，作为最终状态，并把结果之和作为计算结果： add := λx.λy.λs1. 令 (s2,a) = x s1 令 (s3,b) = y s2 (s3,a+b) 这样一来，所有不涉及状态变化的普通操作还可以和原来一样进行，但额外可以增加一些新能力，例如这个操作将当前状态加一，并把旧状态作为计算结果：λs.(s+1,s) 用这些原语可以写出复杂的计算过程，最终得到一个形如 λs1.(s2,a) 的结果，这个结果表示“一旦给定初始状态，就可以算出最终状态和一个结果”，换句话说，是描述了依赖于一个初始状态的一整个计算过程。 Haskell 用这种方法表示和真实世界打交道的 IO 过程。在 Haskell 中有一个特殊的类型，这里为了简化，不妨叫 World，它表示真实世界状态。从键盘读入一行输入的函数 readLn 的类型是 World -> (World, String)，向屏幕输出的函数 putStr 的类型是 String -> World -> (World, ())。这些 IO 过程都需要提供一个 World 才能运行，并且会返回一个新的 World，可以理解为“发生过某个 IO 过程后的世界”。多个 IO 过程可以这样一个接一个地串起来，最终变成 main 函数（它的类型是 World -> (World, ())），表示整个程序的运算规则。 但这个模型其实很有问题，因为 state monad 是支持这种能力的：做一些操作，把状态改变了，并且看到了结果，然后不要新状态了，返回最初的状态和刚刚看到的结果。真实世界中的操作虽然也可以视为不断转换一个状态，但这种状态转换是无法逆转的，用 state monad 来建模它会导致非常荒谬的结果，比如这个函数“假想”自己从键盘上读入一行，但并不真的改变世界状态，然后输出这一行： λworld1. 令 (_, s) = readLn world1 # 注意我们扔掉了 readLn 返回的新的 world putStr s world1 这并没有违反任何类型系统中建立的规则，也没有使用任何一般被认为是“不安全”（unsafe）的操作，所以这样的程序可以顺利通过类型检查并编译😂我以前都没有意识到这个问题，还觉得这套表示 IO 的方式真不错。 感觉应该寻找一种新的、更恰当地建模真实世界中不可逆的操作的方式，但我也不清楚它会是什么样。