（转）Haskell与范畴论

Dear 丶 2022-04-22 07:00 179阅读 0赞

# Haskell与范畴论 #

[http://www.yi-programmer.com/blog/2010-04-06\_haskell\_and\_category\_translate.html][http_www.yi-programmer.com_blog_2010-04-06_haskell_and_category_translate.html]

用haskell的概念解释范畴论。翻译自 wikibook : [http://en.wikibooks.org/wiki/Haskell/Category\_theory][http_en.wikibooks.org_wiki_Haskell_Category_theory]

*  [范畴论简介][Link 1]
    
     *  [范畴公理][Link 2]
     *  [Hask ，Haskell范畴][Hask _Haskell]
 *  [函子][Link 3]
    
     *  [Hask 上的函子][Hask]
     *  [将范畴论的概念对应到Haskell][Haskell]
 *  [Monads][]
    
     *  [示例：幂集函子同时也是monad][monad]
 *  [monad公理和他们的重要性][monad 1]
    
     *  [公理一][Link 4]
     *  [公理二][Link 5]
     *  [公理三和公理四][Link 6]
     *  [应用到do语法][do]
 *  [总结][Link 7]

本文将对范畴论进行简单的介绍，最终目的是为了将它应用到Haskell语言。为了达到这个目的，我们会一边介绍数学上的定义，一边给出对应的Haskell代码。我们并不追求绝对的精确对应，只期望读者在读完以后，能对范畴论的基本概念以及跟Haskell之间的联系有一个直观的感受。

## [范畴论简介][Link 8] ##

![images/Simple-cat.png][images_Simple-cat.png]

一个简单的范畴，由三个对象 *A*, *B* 和 *C* 组成，有三个单位态射 ![id\_A][id_A], ![id\_B][id_B] 和 ![id\_C][id_C] ，还有另外两个态射 ![f : C \\to B][f _ C _to B] 和 ![g : A \\to B][g _ A _to B] 。第三个组成元素（即如何对态射进行组合）没有展示出来。

本质上讲，范畴就是一个组合，它包括三部分：

1.  一组 **对象**
2.  一组 **态射** 。每一个态射捆绑两个对象（一个源对象，一个目标对象）。（也有人把它们叫做箭头，我们这里不这么叫它，因为这个词语在Haskell里面有其他含义。译注：其他含义指的是 Control.Arrow 。）如果 *f* 是一个从源对象 *A* 到目标对象 *B* 的态射，我们把它记作 ![f:A \\to B][f_A _to B] 。
3.  一个叫做 **态射组合** 的概念。如果 *h* 是态射 *f* 和 *g* 的组合，我们记作： ![h=f \\circ g][h_f _circ g] 。

许多事物都构成范畴。比如所有集合就能构成一个范畴 **Set** ，函数（译注：这里说的函数是指集合论中的函数）就是它的态射，态射的组合就是函数的组合。所有群也构成范畴 **Grp** ，保持群结构的函数就是它的态射（群同态），比如任意两个群 *G* 和 *H* ， *G* 的操作符为 :m:\* ， *H* 的操作符是 :m:circ ，那么函数 ![f:G \\to H][f_G _to H] 只要满足如下条件就是一个态射：

![f(u\*v) = f(u)  \\circ  f(v)][f_u_v_ _ f_u_ _circ f_v]

初看起来似乎所有态射都是函数，实际上也不一定，比如下面这个例子，任何偏序结构 (*P*, ![\\leq][leq] ) 都构成范畴，该范畴中的对象就是 *P* 中的元素，任意两个元素 *a* 和 *b* 只要满足 ![a \\leq b][a _leq b] ，那么 ![a \\to a][a _to a] 就是一个态射。另外，在相同的源对象和目的对象之间可以存在多个态射。我们拿 **Set** 范畴为例， ![\\sin][sin] 和 ![\\cos][cos] 都是从 ![R][] 到 ![\[-1,1\]][-1_1] 的函数，但是他们不是相同的态射。

### [范畴公理][Link 9] ###

范畴需要满足三个公理。第一个就是态射的组合操作需要满足结合律。记作：

![f \\circ (g \\circ h) = (g \\circ h) \\circ h][f _circ _g _circ h_ _ _g _circ h_ _circ h]

第二，态射在组合操作下是闭合的。所以如果存在态射 ![f:A \\to B][f_A _to B] 和 ![g:B \\to C][g_B _to C] ，那么范畴中必定存在态射 ![h:A \\to C][h_A _to C] 使得 ![h=f \\circ g][h_f _circ g] 。比如以下面这个范畴为例：

![images/Composition-ex.png][images_Composition-ex.png]

*f* 和 *g* 都是态射，所以我们一定能够对他们进行组合并得到范畴中的另一个态射。那么哪一个是态射 ![f \\circ g][f _circ g] 呢？唯一的选择就是 ![id\_A][id_A] 。类似地， ![g \\circ f=id\_B][g _circ f_id_B] 。

第三个公理，对任何一个范畴 *C* ，其中任何一个对象 *A* 一定存在一个单位态射， ![id\_A:A \\to A][id_A_A _to A] 。这个态射是组合操作的单位元。

![g \\circ id\_A = id\_B \\circ g = g][g _circ id_A _ id_B _circ g _ g]

### [Hask ，Haskell范畴][Hask _Haskell 1] ###

本文重点关注一个叫 **Hask** 的范畴，该范畴由Haskell中所有类型组成，Haskell的函数就是它的态射， (.) 操作符便是态射组合，函数 f::A->B 就是 **Hask** 中的一个从类型 *A* 到类型 *B* 的态射。第一和第三个公理很容易验证通过，因为 (.) 操作符本身就是满足结合律的函数，而且很显然，对于任何函数 f 和 g ， f.g 还是一个函数。在 **Hask** 中，单位态射就是函数 id ，而且显然也满足第三个公理：

id.f = f.id = f

## [函子][Link 10] ##

![images/Functor.png][images_Functor.png]

这是从范畴 ![\\mathbf\{C\}][mathbf_C] 到范畴 ![\\mathbf\{D\}][mathbf_D] 的函子。图中的文字描述了对象 *A* 和 *B* 被转换到了范畴 *D* 中同一个对象，因此，态射 *g* 就被转换成了一个源对象和目标对象相同的态射（不一定是单位态射），而且 ![id\_A][id_A] 和 ![id\_B][id_B] 变成了相同的态射。对象之间的转换是用浅黄色的虚线箭头表示，态射之间的转换是用浅绿色的箭头表示。

OK，我们已经介绍了一些范畴，这些范畴里面都有些对象，还有一些态射能神奇地把对象关联在一起。下面我们要介绍一个范畴论中相当重要的概念，那就是 **函子** ，它甚至能把两个范畴关联在一起。函子本质上说其实就是范畴之间的转换。比如对于范畴 *C* 和 *D* ，函子 ![F : C \\to D][F _ C _to D] 能够：

*  将 *C* 中任意对象 *a* 转换为 *D* 中的 ![F(A)][F_A]
 *  将 *C* 中的态射 ![f : A \\to B][f _ A _to B] 转换为 *D* 中的 ![F(f) : F(A) \\to F(B)][F_f_ _ F_A_ _to F_B]

“健忘”函子就是典型的一个函子： ![\\mathbf\{Grp\} \\to \\mathbf\{Set\}][mathbf_Grp_ _to _mathbf_Set] ，它能将群转换成它底层的集合，并将群的态射转换成集合上的相同行为的函数。另一个例子就是幂集函子： ![\\mathbf\{Set\} \\to \\mathbf\{Set\}][mathbf_Set_ _to _mathbf_Set] ，它能将集合转换成他们的幂集，并将函数 ![f : X \\to Y][f _ X _to Y] 转换成函数 ![\\mathcal\{P\}(X) \\to \\mathcal\{P\}(Y)][mathcal_P_X_ _to _mathcal_P_Y] ，后面这个函数接收所有 ![U \\subset X][U _subset X] 组成的集合（译注：也就是集合 *X* 的幂集），将它转换成 ![f(U)][f_U] ，其中 ![f(U) = \\\{ \\, f(u) : u \\in U \\, \\\}][f_U_ _ _ _ f_u_ _ u _in U _] 。对所有的范畴 *C* 都可以定义一个所谓的单位函子，也叫做 ![1\_C : C \\to C][1_C _ C _to C] ，它将对象和态射直接转换成它们自己。在后面要讲的 [monad公理和他们的重要性][monad 1] 一节中，我们将会看到单位函子的作用。

同样的，函子也需要遵守一些公理。第一，给定一个对象 *A* 上的单位态射 ![id\_A][id_A] ， ![F(id\_A)][F_id_A] 必须也是 ![F(A)][F_A] 上的单位态射，也就是说：

![F(id\_A) = id\_\{F(A)\}][F_id_A_ _ id_F_A]

第二，函子在态射组合上必须满足分配率，也就是说：

![F(f \\circ g) = F(f) \\circ F(g)][F_f _circ g_ _ F_f_ _circ F_g]

### [Hask 上的函子][Hask 1] ###

也许你已经看出来了， typeclass Functor 确实和范畴论中的函子概念关系紧密。首先函子包括两部分：首先它将一个范畴中的对象转换成另一个范畴中的对象，其次它还将一个范畴中的态射转换成另一个范畴中的态射。Haskell中的函子其实是从 **Hask** 到 **Hask** 的子范畴 **Func** 的，范畴 **Func** 是在定义该函子的类型上面的一个范畴。比如函子 list 就是从范畴 **Hask** 到范畴 **Lst** 的函子， **Lst** 范畴只包含一个类型 list ，也就是说函子 list 能将任意类型 T 转换为 \[T\] 。范畴 **Lst** 中的态射就是定义在 list 类型上的函数，即： \[T\]->\[U\] 。那么所有这些东西又如何跟Haskell的 Functor typeclass 联系在一起呢？我们回忆一下 Functor 的定义：

class Functor (f :: * -> *) where
        fmap :: (a -> b) -> (f a -> f b)

我们再定义一个实例：

instance Functor Maybe where
        fmap f (Just x) = Just (f x)
        fmap _ Nothing  = Nothing

关键的来了：type constructor Maybe 将任意类型 T 转换成新类型 Maybe T ，同时定义在 Maybe 上的 fmap 能将函数 a->b 转换为函数 Maybe a->Maybe b 。这样，我们就已经把函子的两个组成部分都定义了，将 **Hask** 中的对象转换到另一个范畴中的对象，并将 **Hask** 中的态射转换到该范畴的态射。所以 Maybe 是一个函子。

对于Haskell的 Functor 一个直观的感觉就是，他们代表了一类可以被map的类型。它可以是 list 或是 Maybe ，也可以是树这样复杂的结构。利用它我们可以编写一个执行实际map操作的函数，和 fmap 组合起来，然后就可以传递任意 Functor 结构给它。比如你可以写一个通用函数可以取代 Data.List.map ， Data.Map.map ， Data.Array.IArray.amap ，等等。

我们继续来看函子公理，多态函数 id 可以替代任意的 ![id\_A][id_A] ，所以第一条公理是满足的：

fmap id = id

直观地看，这句代码的含义是说map一个结构，然后对其中每一个元素啥也不做，和从一开始就啥也不做是等价的。

第二，因为态射组合就是 (.) ，那么：

fmap (f . g) = fmap f . fmap g

这条公理还挺实用。这里我们可以把函子想象成类似 list 这样的容器，等号右边就是一个要遍历容器两遍的算法：首先map这个容器，对其中元素执行函数 g ，产生一个新容器，然后map该新容器，执行 f 。而这条公理告诉我们，这个算法可以换成一个只需遍历一遍的算法，并对其中每一个元素执行 f . g 。这个过程叫做 fusion (译注：fusion啥意思不懂)。

### [将范畴论的概念对应到Haskell][Haskell 1] ###

现在我们来总结一下范畴论的概念要如何转换到Haskell上面呢？ 在这方面 Functor 提供了一个很好的例子。关键在于记住以下几点：

*  我们只探讨 **Hask** 范畴和它的子范畴
 *  范畴的对象就是Haskell的类型
 *  范畴的态射就是Haskell的函数
 *  那些接受类型作为参数并返回另一个类型的东西叫类型构造子
 *  那些接受函数作为参数并返回另一个函数的东西叫高阶函数
 *  typeclass 以及它们提供的多态特性，正好反映了这样一个事实，那就是在范畴论中，其实很多概念都是在一组对象上定义的。

## [Monads][Monads 1] ##

![images/Unit-join.png][images_Unit-join.png]

*unit* 和 *join* ，对monad中每一个对象都必须存在的两个态射

Monad是Haskell中一个相当重要的概念，实际上，它们最开始就是来自范畴论。monad 是一类特别的函子，它们拥有一些独特的结构。monad都是从一个范畴映射到其自身的函子。下面我们来看详细定义，Monad是一个函子 ![M : C \\to C][M _ C _to C] ，并且对于 *C* 中每一个对象 *x* 都存在如下两个态射：

*  ![\\mathit\{unit\}^M\_X : X \\to M(X)][mathit_unit_M_X _ X _to M_X]
 *  ![\\mathit\{join\}^M\_X : M(M(X)) \\to M(X)][mathit_join_M_X _ M_M_X_ _to M_X]

在随后的讨论中，只要不产生混淆，我们就去掉上标 *M* ，只说 ![\\mathit\{unit\}\_X][mathit_unit_X] 和 ![\\mathit\{join\}\_X][mathit_join_X] 。

现在我们来看看它是如何对应到Haskell的typeclass Monad 上的：

class Functor m => Monad m where
        return :: a -> m a
        (>>=)  :: m a -> (a -> m b) -> m b

类型约束 Functor m 可以确保我们已经拥有了函子结构：即对象和态射的一组转换关系。 return 就是对应的 ![\\mathit\{unit\}\_X][mathit_unit_X] 。不过下面我们就遇到问题了，虽然 return 的类型酷似 *unit* ，但 (>>=) 的类型却很难跟 *join* 联系起来。反而下面这样的函数： join :: Monad m => m (m a) -> m a 看起来倒是跟 *join* 挺像的。实际上它们之间是可以互相转换的：

join :: Monad m => m (m a) -> m a
    join x = x >>= id
    
    (>>=) :: Monad m => m a -> (a -> m b) -> m b
    x >>= f = join (fmap f x)

所以给出 return 和 join 和给出 return 和 >>= 是等价的。只不过在范畴论中通常用 *unit* 和 *join* 来定义monad，而Haskell程序员则更喜欢用 return 和 (>>=) \_\[3\] 。范畴论的方式通常要更合理一点，因为对于一个结构 *M* 来说，如果存在一种自然的方式将任意对象 *X* 转换为 ![M(X)][M_X] ，并能将 ![M(M(X))][M_M_X] 转换为 ![M(X)][M_X] ，那么该结构很可能就是一个monad。这一点可以从下面的示例中看出。

### [示例：幂集函子同时也是monad][monad 2] ###

前面描述过的幂集函子 ![P : \\mathbf\{Set\} \\to \\mathbf\{Set\}][P _ _mathbf_Set_ _to _mathbf_Set] 可以形成一个monad。对每一个集合 *S* 都有 ![\\mathit\{unit\}\_S(x) = \\\{x\\\}][mathit_unit_S_x_ _ _x] ，将其中 *S* 的每一个元素映射到只含有该元素的一个集合。注意到这些只有一个元素的集合都是 *S* 的子集，所以 ![\\mathit\{unit\}\_S][mathit_unit_S] 返回的正是 *S* 的幂集中的元素，这样就满足了 monad 对 *unit* 的要求。我们再来定义函数 ![\\mathit\{join\}\_S][mathit_join_S] ，输入为 ![L \\in \\mathcal\{P\}(\\mathcal\{P\}(S))][L _in _mathcal_P_mathcal_P_S] ，它是：

*  *S* 的幂集的幂集的元素.
 *  即 *S* 所有子集组成的集合的所有子集组成的集合的元素 .
 *  即 *S* 的部分子集组成的集合

然后我们返回这些集合的并集, 这样就得到了 *S* 的另一个子集（译注：即 ![P(S)][P_S] 的一个元素，也即成功地从 ![P(P(X))][P_P_X] 映射到了 ![P(X)][P_X] ），公式如下。

![\\mathit\{join\}\_S(L) = \\bigcup L][mathit_join_S_L_ _ _bigcup L]

由此可见 *P* 确实是一个 monad 。

其实 *P* 跟 *\`list\`* 几乎是等价的；除了后者处理的是列表而前者是集合，他们在其他地方基本一致。见表：

<table>       
 <thead> 
  <tr> 
   <th colspan="2">集合上的幂集函子</th> 
   <th colspan="2">Haskell中的List Monad</th> 
  </tr> 
  <tr> 
   <th>类型</th> 
   <th>定义</th> 
   <th>类型</th> 
   <th>定义</th> 
  </tr> 
 </thead> 
 <tbody> 
  <tr> 
   <td colspan="2">给定集合 <em>S</em> 和态射 <img src="http://yntcsb.iteye.com/admin/blogs/imgmath/a225487f82944eb21d7a2b5c47039cb5.png" alt="A \to B"> ：</td> 
   <td colspan="2">给定类型 <cite>T</cite> 和函数 <cite>f :: A -&gt; B</cite> </td> 
  </tr> 
  <tr> 
   <td><img src="http://yntcsb.iteye.com/admin/blogs/imgmath/260a19dc0b406816d44cf2fcf6346dc3.png" alt="P(f):P(A)->P(B)"></td> 
   <td><img src="http://yntcsb.iteye.com/admin/blogs/imgmath/da3f06c1727e9d83778929545c2971db.png" alt="(P(f))(S)={f(a):a \in S}"></td> 
   <td><cite>fmap f :: [A] -&gt; [B]</cite></td> 
   <td><cite>fmap f xs = [ f a | a &lt;- xs ]</cite></td> 
  </tr> 
  <tr> 
   <td><img src="http://yntcsb.iteye.com/admin/blogs/imgmath/f6ffc02c01492f4dfc43da22c0e800a5.png" alt="unit_S:S \to P(S)"></td> 
   <td><img src="http://yntcsb.iteye.com/admin/blogs/imgmath/d1c0867613b4bf9284227964909d6d1e.png" alt="unit_S(X)={X}"></td> 
   <td><cite>return :: T -&gt; [T]</cite></td> 
   <td><cite>return x = [x]</cite></td> 
  </tr> 
  <tr> 
   <td><img src="http://yntcsb.iteye.com/admin/blogs/imgmath/72b03a1fd311f1d4b58b087c02d3e8c4.png" alt="P(P(S)) \to P(S)"></td> 
   <td><img src="http://yntcsb.iteye.com/admin/blogs/imgmath/50cef707a79d3747dd6a3c8c68680de5.png" alt="join_S(L)= \bigcup L"></td> 
   <td><cite>join :: [[T]] -&gt; [T]</cite></td> 
   <td><cite>join xs = concat xs</cite></td> 
  </tr> 
 </tbody> 
</table>

## [monad公理和他们的重要性][monad 3] ##

正如函子需要满足函子的公理，monad也有他们的公理要去满足。我们先把这些公理简单列举一下，并转换成haskell代码，最后再来探讨这些公理的重要性。

给定一个monad ![M:C \\to C][M_C _to C] 和态射 ![f:A \\to B][f_A _to B] 其中 ![A,B \\in C][A_B _in C] ，有公理如下：

1.  ![join \\circ M(join)=join \\circ join][join _circ M_join_join _circ join]
2.  ![join \\circ M(unit)=join \\circ unit=id][join _circ M_unit_join _circ unit_id]
3.  ![unit \\circ f=M(f) \\circ unit][unit _circ f_M_f_ _circ unit]
4.  ![join \\circ M(M(f))=M(f) \\circ join][join _circ M_M_f_M_f_ _circ join]

现在，大家应该可以很自然地把他们转换成下面这样的haskell代码了吧:

1.  join . fmap join = join . join
2.  join . fmap return = join . return = id
3.  return . f = fmap f . return
4.  join . fmap (fmap f) = fmap f . join

(记住，fmap是函子定义中负责转换态射的那一部分。)乍看起来，这些公理似乎看不出存在什么深意。这几条公理究竟有啥鸟含义，凭什么非要monad遵守这几条规定？下面便让我们来探索一二。

### [公理一][Link 11] ###

![images/Monad-law-1-lists.png][images_Monad-law-1-lists.png]

用 list 对公理一进行的演示. 记住在 list monad中 join 就是 concat ， fmap 就是普通的 map 。

为了方便理解这条公理，我们先用 list 作为例子。首先这条公理涉及两个函数， join . fmap join （等式左边）和 join . join (等式右边)。这两个函数的类型是什么呢？因为我们只探讨 list ，所以我们知道 join 的类型是 \[\[a\]\] -> \[a\] ，然后可以推出他们的类型都是： \[\[\[a\]\]\] -> \[a\] 。所以我们的参数是一个 list 的 list 的 list ，然后对这个三层 list 执行 fmap join ，然后再在返回结果上应用 join 。对 list 来说 fmap 就是我们熟悉的普通 map ，所以我们首先对最外层列表的每一个元素进行 join 操作，也就是将其中每一个元素坍缩成为单层 list 。这个时候我们就得到一个 list 的 list ，我们再在其上应用 join ，最终坍缩成为一个 list 。简单地说，我们先进入外层 list ，将第二层和第三层 list 坍缩成一层，然后再将这一层和最外层坍缩成一层。

等式右边又是怎么样一个情况呢？我们首先对我们的三层 list 进行 join ，虽然是三层 list ，但实际上 join 操作的还是两层 list ，因为 \[\[\[a\]\]\] 也可以当作是一个 \[\[b\]\] ，其中 b = \[a\] ，所以，某种意义上说，三层 list 只是内部元素也是 list 的一个两层 list 。所以如果我们将这个 list 的 list （的 list ）应用到 join ，它会将外面两层坍缩成一层，而因为第二层的元素本身还是 list ，所以我们得到的还是一个 list 的 list ，然后我们再应用一次 join ，最终坍缩成为一个 list ，总结起来就是说，等式左边是先坍缩里面两层，然后坍缩外面一层，而等式右边则是先坍缩外面两层，然后里面一层。而这条公理告诉我们，这两个操作应该是等价的。其实也有点像是在说 join 操作需要满足结合律。

Maybe 也是一个 monad，因为：

return :: a -> Maybe a
    return x = Just x
    
    join :: Maybe (Maybe a) -> Maybe a
    join Nothing         = Nothing
    join (Just Nothing)  = Nothing
    join (Just (Just x)) = Just x

所以如果我们有一个三层的 Maybe 类型（举例来说，它可以是 Nothing, Just Nothing, Just (Just Nothing) or Just (Just (Just x)) ），公理一就告诉我们，先坍缩里面两层还是先坍缩外面两层是完全等价的。

### [公理二][Link 12] ###

我们再来看看第二条公理， 同样我们还是用 list 做例子。第二条公理提到两个函数的类型都是： \[a\] -> \[a\] 。等式左边表达的是对一个 list 进行map的函数，将每一个元素 x 转换成者有这一个元素的列表 \[x\]，这样我们最终就得到一个单元素列表组成的列表。然后这个两层 list 通过join函数又重新坍缩回单层 list ，右边部分，接收整个 list \[x, y, z, ...\]，将它转换成单元素 list \[\[x, y, z, ...\]\] ，然后又坍缩成为单层列表。这条公理的含义没那么容易一下子说清楚，不过大概就是说，当你在一个monadic值上面应用return，然后再对见过使用join另它坍缩，不管你是在外层应用return还是在内部应用return，其效果是一样的。

### [公理三和公理四][Link 13] ###

最后两条公理就更加不言而喻了，要展现他们的真实性最简单的方法就是将他们扩展开来：

1.  x -> return (f x) = x -> fmap f (return x)
2.  x -> join (fmap (fmap f) x) = x -> fmap f (join x)

### [应用到do语法][do 1] ###

OK，前面我们已经对monad必须遵守的一些公理进行了一些直观的陈述，但是这些公理为什么如此重要？这个问题的答案当我们看到do语法的时候就清除了。我们知道do只是一个语法糖，它其实就是多个 (>>=) 操作的组合：

do {
           x }                 -->  x -- test
    do {
           let {
           y = v }; x }  -->  let y = v in do {
           x }
    do {
           v <- y; x }         -->  y >>= \v -> do {
           x }
    do {
           y; x }              -->  y >>= \_ -> do {
           x }

另外，我们其实可以通过上面提到的这些公理和 (>>=) 的定义，对 haskell 中的 monad 公理进行证明（证明过程有的地方比较复杂，如果没有兴趣也可以直接跳过）：

1.  return x >>= f = f x 。证明：

return x >>= f
    = join (fmap f (return x)) -- 根据 (>>=) 的定义
    = join (return (f x))      -- 根据公理三
    = (join . return) (f x)
    = id (f x)                 -- 根据公理二
    = f x

1.  m >>= return = m 。证明：

m >>= return
    = join (fmap return m)    -- 根据 (>>=) 的定义
    = (join . fmap return) m
    = id m                    -- 根据公理二
    = m

1.  (m >>= f) >>= g = m >>= (x -> f x >>= g) 。证明（联想 fmap f . fmap g = fmap (f . g) ）：

(m >>= f) >>= g
    = (join (fmap f m)) >>= g                          -- 根据 (>>=) 的定义
    = join (fmap g (join (fmap f m)))                  -- 根据 (>>=) 的定义
    = (join . fmap g) (join (fmap f m))
    = (join . fmap g . join) (fmap f m)
    = (join . join . fmap (fmap g)) (fmap f m)         -- 根据公理四
    = (join . join . fmap (fmap g) . fmap f) m
    = (join . join . fmap (fmap g . f)) m              -- 根据函子的分配率
    = (join . join . fmap (\x -> fmap g (f x))) m
    = (join . fmap join . fmap (\x -> fmap g (f x))) m -- 根据公理一
    = (join . fmap (join . (\x -> fmap g (f x)))) m    -- 根据函子的分配率
    = (join . fmap (\x -> join (fmap g (f x)))) m
    = (join . fmap (\x -> f x >>= g)) m                -- 根据 (>>=) 的定义
    = join (fmap (\x -> f x >>= g) m)
    = m >>= (\x -> f x >>= g)                          -- 根据 (>>=) 的定义

这几条使用 return 和 (>>=) 的monad公理，可以翻译成如下的do语法糖：

<table>     
 <thead> 
  <tr> 
   <th>无参(points-free)风格</th> 
   <th>do语句块</th> 
  </tr> 
 </thead> 
 <tbody> 
  <tr> 
   <td><cite>return x &gt;&gt;= f = f x</cite></td> 
   <td><cite>do { v &lt;- return x; f v } = do { f x }</cite></td> 
  </tr> 
  <tr> 
   <td><cite>m &gt;&gt;= return = m</cite></td> 
   <td><cite>do { v &lt;- m; return v } = do { m }</cite></td> 
  </tr> 
  <tr> 
   <td><cite>(m &gt;&gt;= f) &gt;&gt;= g = m &gt;&gt;= (x -&gt; f x &gt;&gt;= g)</cite></td> 
   <td> 
    <div> 
     <pre>   <span>do</span> <span>{
          </span> <span>y</span> <span>&lt;-</span> <span>do</span> <span>{
          </span> <span>x</span> <span>&lt;-</span> <span>m</span><span>;</span> <span>f</span> <span>x</span> <span>};</span>
       <span>g</span> <span>y</span> <span>}</span>
<span>=</span>
  <span>do</span> <span>{
          </span> <span>x</span> <span>&lt;-</span> <span>m</span><span>;</span>
       <span>y</span> <span>&lt;-</span> <span>f</span> <span>x</span><span>;</span>
       <span>g</span> <span>y</span> <span>}</span>
</pre> 
    </div> </td> 
  </tr> 
 </tbody> 
</table>

现在，monad公理就变成了关于do语句块如何才能正常运转的称述了，如果有一个公理不满足，都会导致用户的困惑，因为do语句块的行为将和你期待的不一样。所以本质上说，monad公理其实是一份关于monad的可用性指南。

## [总结][Link 14] ##

在这一章中，我们一路走到现在，我们知道了范畴是什么，他们对应了haskell的哪些概念。我们介绍了包括函子在内的许多范畴论中的重要概念，同时还介绍了monad这样的高级话题，并且看到了他们对于haskell来说是多么的关键。我们没有介绍范畴论中其他一些基本概念，比如自然转换，因为就我们的目标来说并不需要。我们希望让你能对haskell背后的范畴论概念有一些直观的感受。

[http_www.yi-programmer.com_blog_2010-04-06_haskell_and_category_translate.html]: http://www.yi-programmer.com/blog/2010-04-06_haskell_and_category_translate.html
[http_en.wikibooks.org_wiki_Haskell_Category_theory]: http://en.wikibooks.org/wiki/Haskell/Category_theory
[Link 1]: http://yntcsb.iteye.com/admin/blogs/#id2
[Link 2]: http://yntcsb.iteye.com/admin/blogs/#id3
[Hask _Haskell]: http://yntcsb.iteye.com/admin/blogs/#hask-haskell
[Link 3]: http://yntcsb.iteye.com/admin/blogs/#id4
[Hask]: http://yntcsb.iteye.com/admin/blogs/#hask
[Haskell]: http://yntcsb.iteye.com/admin/blogs/#id5
[Monads]: http://yntcsb.iteye.com/admin/blogs/#monads
[monad]: http://yntcsb.iteye.com/admin/blogs/#monad
[monad 1]: /images/20220422/8d1023052a364ec6a033d4dddc921e78.png
[Link 4]: http://yntcsb.iteye.com/admin/blogs/#id7
[Link 5]: http://yntcsb.iteye.com/admin/blogs/#id8
[Link 6]: http://yntcsb.iteye.com/admin/blogs/#id9
[do]: http://yntcsb.iteye.com/admin/blogs/#do
[Link 7]: http://yntcsb.iteye.com/admin/blogs/#id10
[Link 8]: http://yntcsb.iteye.com/admin/blogs/#id11
[images_Simple-cat.png]: /images/20220422/b5714cf41b9940009190418242eb57d8.png
[id_A]: /images/20220422/1cdb7946686a4ef297ff3daca8e39644.png
[id_B]: /images/20220422/38f778bc9d8f4085ac13e93e64fb52bb.png
[id_C]: http://yntcsb.iteye.com/admin/blogs/imgmath/831718d386401211abede9605461d68f.png
[f _ C _to B]: http://yntcsb.iteye.com/admin/blogs/imgmath/437dc35950ab44fca38bb74e39f81838.png
[g _ A _to B]: /images/20220422/ac8accb29507481ca1431e1da20d26eb.png
[f_A _to B]: /images/20220422/b31fa42e29e04e64b1e9037f6728010c.png
[h_f _circ g]: /images/20220422/b66caf346ae24b5aa9e631cbf78cad81.png
[f_G _to H]: /images/20220422/eb19dba1cc7c4acc8fce85dae29adb41.png
[f_u_v_ _ f_u_ _circ f_v]: /images/20220422/ac177fd0cd644d0faecbb1c2ea120f13.png
[leq]: http://yntcsb.iteye.com/admin/blogs/imgmath/de44c582df9d8d29dbbd70aca311c641.png
[a _leq b]: http://yntcsb.iteye.com/admin/blogs/imgmath/387aef28346a0bfbbba3abe635b2c7df.png
[a _to a]: http://yntcsb.iteye.com/admin/blogs/imgmath/c08246ad81daf6a687675203b72b8a51.png
[sin]: http://yntcsb.iteye.com/admin/blogs/imgmath/5912fc1251cd0c1e212f6dd8d19f17ef.png
[cos]: http://yntcsb.iteye.com/admin/blogs/imgmath/8effff999de692c242b9f7a539c63e58.png
[R]: http://yntcsb.iteye.com/admin/blogs/imgmath/e1e1d3d40573127e9ee0480caf1283d6.png
[-1_1]: http://yntcsb.iteye.com/admin/blogs/imgmath/d060b17b29e0dae91a1cac23ea62281a.png
[Link 9]: http://yntcsb.iteye.com/admin/blogs/#id12
[f _circ _g _circ h_ _ _g _circ h_ _circ h]: /images/20220422/08becde251504c77bf963bd5e031d9e5.png
[g_B _to C]: http://yntcsb.iteye.com/admin/blogs/imgmath/ce30cb45593c0abbd363aa785714eb50.png
[h_A _to C]: http://yntcsb.iteye.com/admin/blogs/imgmath/2015c7079075da44a8eef1285144cc3f.png
[images_Composition-ex.png]: /images/20220422/414916fa1e304939b9420ae165106c2c.png
[f _circ g]: http://yntcsb.iteye.com/admin/blogs/imgmath/c957199199fb6246131b44e53bd5576b.png
[g _circ f_id_B]: /images/20220422/328aa075d2dc4f219cafeab5cf1503f8.png
[id_A_A _to A]: /images/20220422/f2ff5af90cd8465c9aa7dfe2e817f28b.png
[g _circ id_A _ id_B _circ g _ g]: /images/20220422/5ec44c10824e4b1e83bd693003a5a2b0.png
[Hask _Haskell 1]: http://yntcsb.iteye.com/admin/blogs/#id13
[Link 10]: http://yntcsb.iteye.com/admin/blogs/#id14
[images_Functor.png]: /images/20220422/bbdd1579ff12417ba2d008ff4def34eb.png
[mathbf_C]: http://yntcsb.iteye.com/admin/blogs/imgmath/05d05e751a80db7375eae13c25f0ca13.png
[mathbf_D]: http://yntcsb.iteye.com/admin/blogs/imgmath/86e66312d234b4e2a7008b17a7412da4.png
[F _ C _to D]: /images/20220422/7fbef90000ea409cab05d8f2f89565e4.png
[F_A]: /images/20220422/bc88b28efb314353990ae8883d4ac729.png
[f _ A _to B]: http://yntcsb.iteye.com/admin/blogs/imgmath/3ce77e890e47fda3054d5eb796444049.png
[F_f_ _ F_A_ _to F_B]: /images/20220422/163b021c565a425183e5a75d559382b3.png
[mathbf_Grp_ _to _mathbf_Set]: http://yntcsb.iteye.com/admin/blogs/imgmath/4391f88d04db06a9bdac35f0290644f7.png
[mathbf_Set_ _to _mathbf_Set]: http://yntcsb.iteye.com/admin/blogs/imgmath/bebd6024d889c9e281cecf123cbaadeb.png
[f _ X _to Y]: http://yntcsb.iteye.com/admin/blogs/imgmath/8b8a08b3fa6c938ada6dfd602e046cfb.png
[mathcal_P_X_ _to _mathcal_P_Y]: http://yntcsb.iteye.com/admin/blogs/imgmath/1fe26f1dd18323e1804871cbb31c0b88.png
[U _subset X]: http://yntcsb.iteye.com/admin/blogs/imgmath/f16bce057764b9544dd66ca46d8e06dd.png
[f_U]: http://yntcsb.iteye.com/admin/blogs/imgmath/237dccd3133f35c013d7673ca2a706e8.png
[f_U_ _ _ _ f_u_ _ u _in U _]: http://yntcsb.iteye.com/admin/blogs/imgmath/00a3fb333428c79c451d492e93655815.png
[1_C _ C _to C]: http://yntcsb.iteye.com/admin/blogs/imgmath/584a60dce470190d2f4b393b32195b44.png
[F_id_A]: http://yntcsb.iteye.com/admin/blogs/imgmath/1239af8281432fc9a8083d65b00516b1.png
[F_id_A_ _ id_F_A]: /images/20220422/ff383629f3c54dddadd956a0a857001d.png
[F_f _circ g_ _ F_f_ _circ F_g]: /images/20220422/0f5a3066e2aa41fbba90652d151dcb81.png
[Hask 1]: http://yntcsb.iteye.com/admin/blogs/#id15
[Haskell 1]: http://yntcsb.iteye.com/admin/blogs/#id16
[Monads 1]: http://yntcsb.iteye.com/admin/blogs/#id17
[images_Unit-join.png]: /images/20220422/b98b5b5c517444faa7afb04f016679ca.png
[M _ C _to C]: /images/20220422/5702d68108534c328092e22926441c89.png
[mathit_unit_M_X _ X _to M_X]: /images/20220422/5b3148f3e7874420a8278e797f45edaa.png
[mathit_join_M_X _ M_M_X_ _to M_X]: /images/20220422/0cae3daad2224df0a52022d1a09d76b1.png
[mathit_unit_X]: /images/20220422/df963aa7e9a94006a736a2e2744d4484.png
[mathit_join_X]: /images/20220422/55f2ae251abe4349822263a9b728fc34.png
[M_X]: /images/20220422/c653288a6f094f8396874fd685646218.png
[M_M_X]: http://yntcsb.iteye.com/admin/blogs/imgmath/7e44d867d7718baeea17f3d555799d64.png
[monad 2]: http://yntcsb.iteye.com/admin/blogs/#id18
[P _ _mathbf_Set_ _to _mathbf_Set]: http://yntcsb.iteye.com/admin/blogs/imgmath/467393d590d9fd6838125d74e22924c9.png
[mathit_unit_S_x_ _ _x]: http://yntcsb.iteye.com/admin/blogs/imgmath/fb7cefe9f9561da13f83ba9f8132b85a.png
[mathit_unit_S]: http://yntcsb.iteye.com/admin/blogs/imgmath/73b7ba0d3b4ecb55709fb595bbcccaef.png
[mathit_join_S]: http://yntcsb.iteye.com/admin/blogs/imgmath/4af7d133cc5416cb2c35ce3680fee0db.png
[L _in _mathcal_P_mathcal_P_S]: /images/20220422/77bcb996bb2f4e53808e7ff815d55102.png
[P_S]: http://yntcsb.iteye.com/admin/blogs/imgmath/670e000edb9faf3ec289f4790d58fedf.png
[P_P_X]: http://yntcsb.iteye.com/admin/blogs/imgmath/1702ab6256f82d63326e37dfde841beb.png
[P_X]: /images/20220422/5c25e1d7f6b241179c4dcb55a19d542b.png
[mathit_join_S_L_ _ _bigcup L]: /images/20220422/a18fc234e9b046d5ae8c3a5b39041a9b.png
[monad 3]: http://yntcsb.iteye.com/admin/blogs/#id19
[M_C _to C]: http://yntcsb.iteye.com/admin/blogs/imgmath/beb3f916fb7e2ff19ad833143a2aeeb4.png
[A_B _in C]: /images/20220422/e1e0711b1fb84a06b1dafaddf5be3002.png
[join _circ M_join_join _circ join]: /images/20220422/a8c5dd10cb0744fa9cdf16b55b613b51.png
[join _circ M_unit_join _circ unit_id]: /images/20220422/c1548f8d23de416eaa830d3da55131ea.png
[unit _circ f_M_f_ _circ unit]: /images/20220422/734fde65dcc340958e61d2d66e78dded.png
[join _circ M_M_f_M_f_ _circ join]: /images/20220422/8e8c03aee47b4522876ae898a9e018a8.png
[Link 11]: http://yntcsb.iteye.com/admin/blogs/#id20
[images_Monad-law-1-lists.png]: /images/20220422/8930b3e9642847d89a78b155c7d56b26.png
[Link 12]: http://yntcsb.iteye.com/admin/blogs/#id21
[Link 13]: http://yntcsb.iteye.com/admin/blogs/#id22
[do 1]: http://yntcsb.iteye.com/admin/blogs/#id23
[Link 14]: http://yntcsb.iteye.com/admin/blogs/#id24