计算概论 A 课程笔记：范畴论与 Monad 部分

Last updated on November 15, 2023 5:00 PM

Preface

因为我觉得我要沉淀下期中了所以自己记给自己看一下。

不保证内容的可读性，因为懒得去想对应语言的表达所以中英文夹杂了一下。

不保证内容的正确性，如果能帮忙指出错误，感激不尽。

Functor

Definition

一个定义在两个范畴 $\mathsf C,\mathsf D$ 上的 functor $F:\mathsf C\to\mathsf D$ 包含以下两种操作：

对象之间的映射。

即将 $\mathsf C_0$ 中的每个对象映射到 $\mathsf D_0$ 中，可以记作 $F~a$ 。
态射之间的映射。

即将 $\mathsf C_1$ 中的每个态射 $f_{a\to a'}$ 映射到 $\mathsf D_1$ 中的 $g_{F~a\to F~a'}$ 上，可以记作 $F~f$ 。

需要满足两条公理：

$\forall a\in \mathsf C_0, F~1_a = 1_{F~a}$
$\forall f_{a\to b},g_{b\to c}\in \mathsf C_1, F~g\circ F~f = F~(g\circ f)$ 。

并且，一个满足 $\mathsf C = \mathsf D$ 的 functor $F_{\mathsf C\to\mathsf D}$ 被称为 endofunctor（自函子）

Examples

$1_C$

很蠢的“单位函子”，不说了。两条公理是自明的。
$P_{\mathsf{Fn}\to\mathsf{Fn}}$

$P~a~\dot=~\{x\mid x\subseteq a\}$

$P~f_{a\to b}~\dot=~\{x\mapsto \{f ~i \mid i\in x\}\mid x\in P~a\}$

类似于幂集的感觉。

两条公理的证明不是重点~~而且我也不太会~~略过。

What about in Haskell

class Functor f where
  fmap :: (a -> b) -> (f a -> f b)
-- which satisfies
-- Identity:    fmap id == id
-- Composition: fmap (f.g) == fmap f . fmap g

可以发现，f 不就是 $\mathsf {Fn}_0\to \mathsf {Fn}_0$ 的一个 object-mapping 吗，fmap 不就是 $\mathsf{Fn}_1\to \mathsf{Fn}_1$ 的一个 morphism-mapping 吗。这两个东西组合起来，就是一个很良定义的 functor。

补充：这两个 law 实际上就是保证了“范畴的结构不会被改变”这件事情。

而且可以证明，For any parameterized type in Haskell, there is at most one function fmap that satisfies the required laws. 具体怎么证明我也不知道。

因为 Haskell 中我们都是研究“函数”，所以我们研究的范畴为 $\mathsf{Fn}$ 。而且我们发现， $F$ 是一个 endofunctor。

下面举几个例子，例如 Maybe：

data Maybe a = Nothing | Just a

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

再比如说树

data Tree a = Leaf a | Node (Tree a) (Tree a)
			deriving Show

instance Functor Tree where
  fmap g (Leaf x) = Leaf (g x)
  fmap g (Node l r) = Node (fmap g l) (fmap g r)

是不是感觉具体了一些，此时我们可以把 functor 大概理解为一个“结构”或者说“壳子”。将抽象层级再次提高了。例如说所谓的 inc 函数，利用 functor 我们可以定义为

1 2	`inc :: Functor f => f Int -> f Int inc = fmap (+1)`

注意到，刚才提到的 functor 的两条 law 保证了整个的 structure 没有改变，例如我们对于 functor []，用 fmap 操作之后，元素个数不会增加/减少，顺序不会改变，都是一一对应的。

Natural Transformation

坑着。

Applicative

后记：为啥要叫 applicative，大抵是因为他做到了更广泛的 function application 的映射罢。。。。

Introduction

In retrospect, we know functors abstracts the idea of mapping a function over each element of a structure。

现在若我们想解决含有更多参数的函数，怎么办呢？

fmap0 :: a -> f a
fmap1 :: (a -> b) -> f a -> f b
fmap2 :: (a -> b -> c) -> f a -> f b -> f c
fmap3 :: (a -> b -> c -> d) -> f a -> f b -> f c -> f d

如果我们能利用 curried function 的想法，将如上的东西也抽象，定义一个更加 generalized 的 fmap，岂不是很好？

这样子考虑，引入两个函数：

1 2	`pure :: a -> f a (<*>) :: f (a -> b) -> f a -> f b`

注意。 <*> 运算符是具有左结合性的，正如我们的 function application 一样。他能帮我们做到什么事情呢？注意看下面的代码：

fmap0 :: a -> f a
fmap0 = pure

fmap1 :: (a -> b) -> f a -> f b
fmap1 g x = pure g <*> x
-- fmap1 g x = g <$> x

fmap2 :: (a -> b -> c) -> f a -> f b -> f c
fmap2 g x y = pure g <*> x <*> y
-- fmap2 g x y = g <$> x <*> y
-- 类型解读：
-- g :: (a -> b -> c)
-- x :: f a
-- y :: f b
-- pure g <*> x :: f (a -> (b -> c)) -> f a -> f (b -> c)
-- 注：一开始没有想清楚是因为没有把 (b -> c) 当成一个整体看待
-- 所以我们拿到了这个 f (b -> c) 的类型后，继续往右结合。
-- (pure g <*> x) <*> y :: f (b -> c) -> f b -> f c
-- 整件事情是不是就变得合理了起来

fmap3 :: (a -> b -> c -> d) -> f a -> f b -> f c -> f d
fmap3 g x y z = pure g <*> x <*> y <*> z
-- fmap3 g x y z = g <$> x <*> y <*> z

注：其中 <$> 运算符被定义为

(<$>) :: Functor f => (a -> b) -> f a -> f b
-- It's an infix synonym for fmap
-- 作为对比，让我们看看之前学过的 function application operator：
($) ::                (a -> b) -> a -> b

于是我们可以给出 applicative 的定义：

class Functor f => Applicative f where
  -- lift a value
  pure :: a -> f a
  -- sequential application
  (<*>) :: f (a -> b) -> f a -> f b

Examples

Let’s slow down for a while to see how we can make some known types into applicative functors.

instance Applicative Maybe where
  pure = Just
  
  Nothing <*> _ = Nothing
  (Just g) <*> mx = fmap g mx

instance Applicative [] where
  pure x = [x]
-- (<*>) :: [a -> b] -> [a] -> [b] 
  gs <*> xs = [g x | g <- gs, x <- xs]

这个可以理解为 pure transforms a value into a singleton list, while <*> takes a list of functions and a list of
arguments, and applies each function to each argument in turn, returning all the results in a list. （我直接抄的书懒得管那么多了）

1 2	`> pure () <> [1,2] <*> [3,4] [3,4,6,8]`

看这一段代码吧，实际上，pure (*) <*> [1,2] 即为 [(1*), (2*)]，然后再和 [3,4] 复合的话就是（前面的是外层循环，后面的是内层循环）。

利用 list 的 applicative 性，我们可以改写一些函数来避免中间变量的书写，例如

1
2
3

prod :: [Int] -> [Int] -> [Int]
-- prod xs ys = [x * y | x <- xs, y <- ys]
prod xs ys = (*) <$> xs <*> ys

最后来看一下之前遇到过的 IO 类型。

instance Applicative IO where
  pure = return
  
  mg <*> mx = do {g <- mg; x <- mx; return (g x)}

可能有点抽象，看个例子先吧。

1
2
3

getChars :: Int -> IO String
getChars 0 = return []
getChars n = pure (:) <*> getChar <*> getChars (n - 1)

Applicative 与副作用的思考

一开始我们定义 applicative 实际上是想要达到某种“将多参数的函数进行映射”的想法。

但是其实我们可以将其视作一种，programming with effects 的 approach（我不想翻译了，对不起）

什么意思呢？有没有注意到，被 applicative functor 包裹起来的这个整体，是不是或多或少带点副作用而不是单纯的 plain value 了。例如 Maybe 就是说，有可能失败；IO 则是可能涉及到 IO 操作。

所以说，applicative 在做的事情，也可以理解为 applying pure functions to effectful arguments，具体是什么 effect 取决于 functor。

标准库里面定义了如下的一个 generic function：

1
2
3

sequenceA :: Applicative f => [f a] -> f [a]
sequenceA [] = pure []
sequenceA (x:xs) = pure (:) <*> x <*> sequenceA xs

就是说，将一系列的 applicative 操作变成了一个，同时返回一个返回值的列表。比如说我们刚才的 getChars 就可以被定为为

1 2	`getChars :: Int -> IO String getChars = sequenceA [replicate n getChar]`

是不是，重复 $n$ 次读入字符这个操作，然后把结果合并，很合理吧。

Applicative Laws

pure id <*> x = x
pure (g x) = pure g <*> pure x
x <*> pure y = pure (\g -> g y) <*> x
x <*> (y <*> z) = (pure (.) <*> x <*> y) <*> z

分别注解一下。

第一行比较显然，不解释。分析类型：id :: a -> a，x :: f a

第二行说的就是，function application 在 pure 之后仍得到保留，分析类型：pure (g x) :: f b，g :: a -> b

（存疑）第三行比较有趣。说的是如果我们将一个 effectful function 应用到一个 pure 的参数上时，先处理哪部分是无关紧要的。请注意这里 x 的类型是 f (a -> b)，y 的类型是 a，g 是一个 lambda function，其类型为 a -> b，所以在 pure 了之后，pure (\g -> g y) 的类型为 f ((a -> b) -> b)，后面再接一个 x :: f (a -> b) 其实就相当于是把 x 作为参数。

第四行，分析类型吧。z :: f a，y :: f (a -> b)，x :: f (b -> c)，(pure (.) <*> x <*> y) :: f (a -> c)。

~~至于为什么要有这些 law，存疑。等周三上课吧。~~老师也不太会，没事了。

好他妈难啊。

Monad

Kleisli Category

背景是实现所谓的 logging，即对于一个函数，我们让他需要同时打印一段 log。

于是我们定义了下面的这个东西：

type Writer a = (a, String)

(>=>) :: (a -> Writer b) -> (b -> Writer c) -> (a -> Writer c)
m1 >=> m2 = \x -> let (y, s1) = m1 x
                      (z, s2) = m2 y
                  in (z, s1 ++ s2)

return :: a -> Writer a
return x = (x, "")

我们是从范畴 $\mathsf{Fn}$ 出发构建我们的 $\mathsf{Writer}$ 范畴的。对象保持不变，但是态射从原来的 function 变成现在的 embellished function。

embellished function 其实可以理解为，带副作用的函数。比如说这里要实现的功能就是在正常计算值的基础上，完成 logging 的过程。

这个时候我们还是将 embellished function 理解为 a -> b 的态射，虽然他实际上是一个 a -> m b 的函数。不过我们是可以良定义出态射的复合的，也就是上面的 >=> 符号。

同时，单位态射也得到了定义，上面的 return。

再次重申，这篇文章是给我自己看的。

上面的 $\mathsf{Writer}$ 范畴就是 Kleisli Category —— 基于 Monad 的范畴的一个例子。这里还是先直接给出形式化定义吧。

给定一个范畴 $\mathsf C$ 和一个自函子 $m: \mathsf C\to \mathsf C$ ，则其对应的 Kleisli 范畴 $\mathsf K$ 是如下定义的：

$\mathsf K_0~\dot=~\mathsf C_0$
$\mathsf K_1 ~\dot=~ \{f_{a\to b}\mid f_{a\to b}\text{ is a morphism }f'_{a\to m~b}\text{ in }\mathsf C_1\}$

这句话可能有些不好理解，等一下会说。
$\operatorname{dom}$ 和 $\operatorname{sub}$ 的定义略。
$1_a ~\dot=~ \mathsf{return}_{a\to m~a}$ ，其中 $\mathsf{return}_{a\to m~a}\in\mathsf C_1$
$(g_{b\to c}\circ f_{a\to b})_{a\to c}~\dot=~f'\rightarrowtail g'$ ，其中 $\rightarrowtail$ 是一个复合操作，其对于 $\mathsf C_1$ 中的态射 $f'_{a\to m~b},g'_{b\to m~c}$ 给出了一个其复合后的态射 $h'_{a\to m~c}\in\mathsf C_1$ 。

满足如下两条公理：

Unit： $f\circ 1=f=1\circ f$
Associativity： $h\circ (g\circ f) = (h\circ g)\circ f$ 。

之前没有理解的地方是 $\mathsf K_1$ 的定义。实际上呢，可以理解为，我们对于 $\mathsf C_1$ 中的态射 $f'_{a\to m~b}$ ，将其就视为是 $\mathsf K_1$ 中 $a\to b$ 的态射。他实际上做的事情是 $a\to m~b$ ，但是在 $\mathsf K$ 中就把他视为 $a\to b$ 的态射。

然后定义了那个小鱼符号之后，态射的复合就也是良定义的了。

不知道这么说够不够清楚。

然后， $m$ 这个 functor 就是一个 monad。

All told, a monad in X is just a monoid in the category of endofunctors of X, with product × replaced by composition of endofunctors and unit set by the identity endofunctor.

In Haskell

我们其实没有定义小鱼符号。因为其也不是那么的简洁，instead，我们定义 bind。

1	`(>>=) :: m a -> (a -> m b) -> m b`

笔记 > 本科课程

#笔记 #Haskell #函数式编程

计算概论 A 课程笔记：范畴论与 Monad 部分

https://blog.imyangty.com/note-intro2computing/CT/

Author

YangTY

Posted on

October 22, 2023

Licensed under

一些高数积分笔记 Previous

Latex 细碎笔记整理 Next

计算概论 A 课程笔记：范畴论与 Monad 部分

Preface

Category

Definition

Some Examples of Category

Some Trivial Ones

Fn

Some Extra Definitions

Groupoid, Group and Monoid

Functor

Definition

Examples

What about in Haskell

Natural Transformation

Applicative

Introduction

Examples

Applicative 与副作用的思考

Applicative Laws

Monad

Kleisli Category

In Haskell