Venns' Space

Haskell和范畴论(下) – Monad

 计算机  2796  6 分钟

这篇文章的前半部分在暑假的时候就已经写好，后面忙于考托福，就一直没有继续写下去。最近有时间了，突然发现已经到年末了，遂找了个周末将这篇文章写完。

前言

本文是上一篇文章 Haskell和范畴论(上) 的下篇, 主要介绍 Haskell 中最神秘, 最挠有趣味的 Monad 的概念.

Haskell is pure

Haskell 中的函数都是纯粹的, 所谓纯粹是指 Haskell 中所有的函数是数学意义上的映射, 输入同一个数, 输出的值也必定相同. 而在C语言中, 由于有全局变量, 静态变量等, 函数的输出可能会随外部环境改变而改变, 因而不是纯粹的.

1
2
3
4
5

int countAdd(int x)
{
  static int counter = 0;
  return x + (counter++);
}

如上所示 countAdd(x) 函数的值会随调用次数的改变而改变, 从而不是纯的.

Haskell 中的函数是纯的, 这类似于数字电路中的组合逻辑. 而命令式编程语言, 如C, 由于具有状态变量, 具有某种程度上的记忆性, 因而不是纯的, 非纯的函数类似与数字电路中的时序逻辑.

一般计算机的抽象使用图灵机, 也就是带有状态的有限自动机. 要实现一般的编程, 总要涉及到状态变量, 这类非纯的东西. 另外 IO 可以看作一组公用的寄存器, 它天生就是一个全局变量, 涉及 IO 操作的将导致非纯的函数.

那么如何使用 Haskell 中的函数表达常见的非纯的函数呢, 或者说如何表达带有 副作用(side-effect) 的函数呢. 答案是 Monad , 尤其是其中的 State Monad. State Monad 可以看作将时序逻辑展开成组合逻辑.

Computation with Effects

本节按照 Moggi 文章 <&moggiNotionsComputationMonads> 的思路介绍 Monad .

给定一个类型 \(A\) , 用 \(T A\) 表示带有副作用的 \(A\) 类型值. 而带有副作用的函数则可表示为类型 \(f :: A \rightarrow T B\) . 一般的程序可以看作特殊的函数, 因而, 这种计算表示, 也给出了一般的程序的抽象.

给定一个 \(A\) 类型的参数, 我们应当可以将 \(A\) 包裹进 \(T A\) 中, 由于没有进行其他作用, 进行这个操作的函数应当没有什么副作用, 虽然, 形式上 \(TA\) 是带有副作用的. 这个函数就是 Haskell 中的 pure :: a -> T a 函数.

如果有两个程序 \(f : A \rightarrow T B, g : B \rightarrow T C\), 那么这两个程序应当可以组合起来, 得到一个 \(A \rightarrow T C\) 的程序. 这就是 Haskell 中的 >=> :: (a -> T b) -> (b -> T c) -> (a -> T c) .

实际上 pure, (>=>) 两个函数可以构成一个范畴, 称之为 Kleisi Category. 具体定义如下

  • 所有的类型是 Kelisi 范畴中的对象
  • pure:: a -> T a 是这个范畴中对象 a 的 Id 态射
  • f:: a -> T b 是这个对象中 \(a \rightarrow b\) 的态射
  • f >=> g 是两个态射 \(f \in \mathrm{Hom}(A,B), g \in \mathrm{Hom}(B,C)\) 的合成.

要满足范畴的要求, 还需一些约束, 他们是

  • 恒等性: pure >=> f = f
  • 恒等性: f >=> pure = f
  • 结合性: f >=> (g >=> h) = (f >=> g) >=> h

实际上述的 pure, (>=>) 两个函数可以用 pure, (>>=) :: T a -> (a -> T b) -> T b 等价描述. 二者的相互转化由下列公式给出

1
2
3
4
5

(>=>) :: (a -> T b) -> (b -> T c) -> (a -> T c)
(>=>) f g = \x -> f x >>= g

(>>=) :: T a -> (a -> T b) -> T b
(>>=) x f = (const x >=> f) x -- x can be replced by any value

>>= 读作 "bind" , 它可以看作将一个程序 a-> T b 提升为 T a -> T b 的算子. 使得原本的 函数能够接受一个带副作用的输入. 这就是 Haskell 中 Monad 的定义.

由此引出 Kleisi Triple 的定义 <&moggiNotionsComputationMonads> .

Kleisi Triple

Kleisi Triple 就是有上述的 T, pure, >>= 定义的三元组. 他们用来抽象带副作用的程序, 唯一的确定了一个 Kleisi Category. 我们重新用数学符号表示该三元组. \((T, \eta , -^*)\) 是范畴 \(\mathcal C\) 上的 Kleisi Triple 如果下述定义

  • \(T: \mathrm{Obj}(\mathcal C) \rightarrow \mathrm{Obj}(\mathcal C)\)
  • \(\eta_A: A \rightarrow T A, \forall A \in \mathrm{Obj}(\mathcal C)\)
  • \(f^*:T A \rightarrow T B, \forall f: A \rightarrow T B\)

满足:

  • \(\eta_A^* = \mathrm{id}_{TA}\)
  • \(f^* \circ \eta_A = f, f : A \rightarrow T B\)
  • \(g^* \circ f^* = (g^* \circ f)^*, f : A \rightarrow T B, g : B \rightarrow T C\)

Kleisi Triple 是更适合编程的语言, 实际上述的定义就是数学家们所说的 Monad .

Monad

Monad 是范畴论中的一个术语, 它和 Kleisi Triple 是等价的.

三元组 \((T,\eta,\mu)\) 是范畴 \(\mathcal C\) 上的 Monad ,如果

  • \(T\) 是 \(\mathcal C\) 到 \(\mathcal C\) 的自函子.
  • \(\eta: \mathrm{Id}_\mathcal{C} \rightarrow T\) 是自然变换
  • \(\mu: T^2 \rightarrow T\) 是自然变换

使下面的交换图交换:

给定一个 Kleisi Triple 可以定义出一个 Monad 其中:

  • \(T(f):= (\eta_B \circ f)^*, f:A \rightarrow B\)
  • \(\eta\) 定义相同
  • \(\mu_A:=(Id_{TA})^*\)

同样给定一个Monad也可定义出一个 Kleisi Triple

  • \(T\) 就是Monad中Functor 在对象上的约束（Kleisi Triple中的 \(T\) 不需要是Functor）
  • \(\eta\) 定义相同
  • \(f^*:= \mu_B \circ T(f),f:A \rightarrow TB\)

Examples

Monad的理论基本介绍完了, 接下来就是介绍实际的一些用来表示副作用的 Monad 了.

Maybe Monad

Maybe Monad 几乎是Trival的，其实现如下：

1
2
3
4

instance Monad Maybe where
  return = Just
  (>>=) Nothing _ = Nothing
  (>>=) (Just x) f = f x

Maybe Monad 可以轻松拓展为处理 Exception 的Monad，只要将 其中的 Nothing 换成另一个包含多种错误的 Sum Type 即可。

State Monad

比较有趣的是 State Monad。State Monad 的形式定义是 \(TA = (A \times S)^S\) \((A \times S)^S\) 是所有形如 \(f:S \rightarrow (A \times S)\) 函数的集合。写成用Haskell的语法可以给出State Monad的定义

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

data State s a = State {runState :: s -> (a,s)}

instance Monad State s where
  return x = State $ \s -> (x,s)
  (>>=) mx f = State $ \s ->
    let
      (a',s') = runState mx
      my = f a'
    in
      runState my s'

可以发现 State Monad 类似一个带输出的状态机，它由他的状态转移函数 ( s->s ) 决定,该状态机的输出是附带的，状态转移函数是本质的。那么 a -> State s b 代表什么样的语义呢？它是根据输入值 a （严格来说是 a 类型的值）输出一个带输出的状态转移函数，从而不同的输入值可以决定不同的状态跳转方式。如果按照前述 Kleisi Triple 的方式来理解, a -> State s b 是 Kleisi Triple 中的 \(A \rightarrow TB\) ,它应该比 State s b 类型的变量更重要。当两个 Kleisi 范畴中的箭头合成时，比如 a -> State s b 与箭头 b -> State s c 合成第二个箭头首先读取第一个箭头的输出，也就是状态机跳转后的输出，然后这一输出值将传递给第二个箭头，然后决定第二次状态跳转方式。这恰恰就是图灵机的模型，图灵机是个有限状态机，它不断读取纸带输入，然后根据输入决定状态跳转。从而借助 State Monad 我们验证了Haskell是图灵完备的。

IO Monad

IO Monad在 Haskell 中一般当作黑盒使用。在 Moggi 论文中，IO也是一种 Monad，但它的抽象不同与Haskell 中的实现。输入可以抽象为Kleisi Triple : \(TA:= \mu\gamma . A + \gamma^U\) 其中的 \(\mu\) 是 Recursive Type 的写法<&pierceTypesProgrammingLanguages2002>. 其中的加号表示一个 Sum Type .从而 \(TA\) 要么是A类型本身，要么是 U \rightarrow A 类型，假设 U 是输入类型。用Haskell 表示就是

1

data T a = T a | Box {unBox :: (U -> (T a))}

这是一个很有意思的一个类型它包含了所有形如 U -> A , U->U->A ,.., U->U->... ->U->A 假设 U 代表键盘上的字母表， TA 则代表了键盘不同输入是对程序的影响。将它定义为一个Monad的时候，Kleisi Triple的箭头是将这些 U 输入接起来。

在 Moggi 论文中，输出被抽象为 \(TA := \mu\gamma. A+(U \times \gamma)\). \(U\times \gamma\) 是 Product Type 和前文类似，该抽象也非常有意思。分析同前文。

上述的对IO的抽象非常和现实非常贴切，但是不太实用。实际上 IO 可以用 State Monad 的实现。计算机可以看作一个巨大的有限状态机这些状态就是CPU中的一些寄存器。同样 IO 操作可以看作是对这些寄存器的读与写。那么只要将与IO相关的寄存器纳入到 State Monad 中的状态中，便可实现IO操作。当然，实际实现中不必操作寄存器，只要对基本的读写操作封装好，设计相应状态变化时便使用该封装好的函数即可。

参考 Tsoding 的视频，他将 IO 定义为如下的State Monad

1
2

data World = World
data IO a = IO{ runIO :: World -> (a, World)}

然后便可实现相应的IO操作，唯一需要注意的是 World 更多意义是形式上的，它保证了IO执行的严格顺序，但是由于 Haskell是Lazy的，可能不对 World 执行显示计算，那么IO的顺序之间的依赖可能被打断。因此，在实行具体的IO操作时 World 要进行显示计算。具体可参考Youtube的视频。

<~/Documents/mybib.bib>

updatedupdated2025-01-122025-01-12

相关文章：