Skip to content

Latest commit

 

History

History
809 lines (599 loc) · 27.7 KB

part1.org

File metadata and controls

809 lines (599 loc) · 27.7 KB

COMMENT

(require 'ob-dot)

{{{ruby(猫论,Catergory Theory)}}}

./images/Cheshire_Cat.png [fn:1]

`But I don’t want to go among mad people,’ Alice remarked.

`Oh, you can’t help that,’ said the Cat: `we’re all mad here. I’m mad. You’re mad.’

`How do you know I’m mad?’ said Alice. `You must be,’ said the Cat, `or you wouldn’t have come here.’

Alice didn’t think that proved it at all; however, she went on `And how do you know that you’re mad?’

– Alice’s Adventures in Wonderland

{{{ruby(单子,Monad)}}}是什么? 你也不懂, 我也不懂, 我们都不懂.

话说, 我又怎么知道你不懂呢?

当然不懂, 不然, 你怎么会来到这里?

我又是怎么知道自己不懂呢?

因为，我知道懂的人是什么样子. 显然, 我不是.

因为，懂的人一定知道{{{ruby(猫论,Category Theory)}}}.

这一部分主要是纯理论，这里面有很多很装的单词，比如 {{{ruby(单子,Monad)}}}/，它们都是 /斜体 ，就算一遍没看懂[fn:13]，把这些词背下来也足够装好长一阵子逼了。

这里还有很多代码, 它们都成对出现, 通常第一段是 Haskell, 第二段是 Scala 3.[fn:14]

{{{ruby(范畴,Category)}}}

对于计算机科学的学生，范畴并不是一个新的概念，在本科大纲里，大家都应该学过 离散数学（Discrete Mathematics） ，其中会讲很多 集合论（Set Theory） 图论，抽象代数的东西。 现在回头看看，其实也就是集合论和抽象代数的内容。

所以下面的概念都点到为止，只为解释写成代码会长什么样。

一个 {{{ruby(范畴,Category)}}} 包含两个玩意:

  • 东西 O （Object）
  • 两个东西的关系，箭头 ~> （ {{{ruby(态射,Morphism)}}} ）

还必须带上一些属性:

  • 一定有一个叫 id 的箭头，也叫做 1
  • 箭头可以 {{{ruby(组合, compose)}}}

恩, 就是这么简单!

images/category.png

注意到为什么我会箭头从右往左，接着看代码, 你会发现这个方向跟 compose 的方向刚好一致!

这些玩意对应到 Haskell 的 Typeclass 大致就是这样:

class Category (c :: * -> * -> *) where
  id :: c a a
  (.) :: c y z -> c x y -> c x z

如果这是你第一次见到 Haskell 代码，没有关系，语法真的很简单：

  • class 定义了一个 TypeClass， Category 是这个 TypeClass 的名字
  • Type class 类似于定义类型的规范，规范为 where 后面那一坨
  • 类型规范的对象是参数 (c:: * -> * -> *) ， :: 后面是c的类型
  • c 是 higher kind * -> * ，跟higher order function的定义差不多，它是接收类型，构造新类型的类型。这里的 c 接收一个类型，再接收一个类型，就可以返回个类型。
  • id:: c a a 表示 c 范畴上的 a 到 a 的箭头
  • . 的意思 c 范畴上，如果喂一个 y 到 z 的箭头，再喂一个 x 到 y 的箭头，那么就返回 x 到 z 的箭头。

而 Scala 可以用 trait 来表示这个 typeclass:

trait Category[C[_, _]] {
  def id[A]: C[A, A]
  def <<<(a: C[Y, Z], b: C[X, Y]): C[X, Z] 
}

如果这是你第一次见到 Scala 代码，没关系，从Haskell可以飞快的切换过来：

  • class -> trait
=c
* -> * -> *= -> C[_, _]
  • :: -> :
  • 函数名前加 def

另外 compose 在 haskell 中直接是句号 .

scala 中用习惯用 <<< 或者 compose

总之，我们来用文字再读一遍上面这些代码就了然了.

范畴 C 其实就包含：

  1. 返回 A 对象到 A 对象的 id 箭头
  2. 可以组合 Y 对象到 Z 对象 和 X 对象到 Y 对象的箭头 compose

简单吧？还没有高数抽象呢。

Hask

Haskell 类型系统范畴叫做 Hask。

在 Hask 范畴上：

  • 东西就是类型
  • 箭头是类型的变换，即 ->
  • id 就是 id 函数的类型 a -> a
  • compose 当然就是函数组合的类型
type Hask = (->)
instance Category (Hask:: * -> * -> *) where
  id a = a
  (f . g) x = f (g x)

我们看见新的关键字 instance ，这表示 Hask 是 Type class Category 的实例类型，也就是说对任意Hask类型, 那么就能找到它的 id 和 compose

given Category[=>[_, _]] {
  def id[A]: A => A = identity[A]
  def <<<[X, Y, Z](a: Y => Z, b: X => Y) = a compose b
}

Scala 中, 只需要 new 这个 trait 就可以实现这个 typeclass

其中: identity Hask a a 就是

(->) a a -- or
a -> a -- 因为 -> 是中缀构造器
A => A

Duel

每个 Category 还有一个镜像，什么都一样，除了箭头是反的。

函子 / Functor

两个范畴中间可以用叫 Functor 的东西来连接起来，比如一个从范畴 C 到范畴 D 的函子 T，我们可以标 作 Functor C D T 。

#+Functor Category

images/functor.png

所以大部分把函子或者单子比喻成盒子其实在定义上是错的，虽然这样比喻比较容易理解，在使用上问题也不大。但是，函子只是从一个范畴到另一个范畴的箭头而已。

  • 范畴间东西的函子标记为 T(O)
  • 范畴间箭头的函子标记为 T(~>)
  • 任何范畴 C 上存在一个 T 把所有的 O 和 ~> 都映射到自己，标记为函子 1_C
    • 1_C(O) = O
    • 1_C(~>) = ~>
class (Category c, Category d) => Functor c d t where
  fmap :: c a b -> d (t a) (t b)
trait Functor[C[_, _], D[_, _], T[_]]:
  def fmap[A, B](c: C[A, B]): D[T[A], T[B]]

Functor c d t 这表示从范畴 c 到范畴 d 的一个 Functor t

如果把范畴 c 和 d 都限制到 Hask 范畴：

class Functor (->) (->) t where
  fmap :: (->) a b -> (->) (t a) (t b)
trait Functor[=>[_, _], =>[_, _], T[_]]:
 def fmap[A, B](c: =>[A, B]): =>[T[A], T[B]]

-> 或者 => 可以写在中间的:

这样就会变成我们熟悉的函子定义：[fn:5]

class Functor t where
  fmap :: (a -> b) -> (t a -> t b)
trait Functor[T[_]]:
  def fmap[A, B](c: A => B): T[A] => T[B]

而 {{{ruby(自函子,endofunctor)}}} 就是这种连接相同范畴的 Functor，因为它从范畴 Hask 到达同样的范畴 Hask。

这回看代码就很容易对应上图和概念了, 这里的自函子只是映射范畴 -> 到 ->, 箭头函数那个箭头, 类型却变成了 t a 。

这里的 fmap 就是 T(~>)，在 Hask 范畴上，所以是 T(->), 这个箭头是函数，所以也能表示成 T(f) 如果 f:: a -> b

{{{ruby(Cat,猫)}}}

递归的, 当我们可以把一个范畴看成一个对象，函子看成箭头的话，那么我们又得到了一个新的范畴，这种对象是范畴箭头是函子的范畴我们叫它 – {{{ruby(Cat,猫)}}} 。

已经{{{ruby(没,meow)}}}的办法用语言描述这么高维度的事情了，请回忆<<Functor Category>>并把 C 和 D 想象成点。

自然变换 / Natural Transformations <<NT>>

函子是范畴间的映射，所以如果我们现在又把 Cat 范畴看成是对象, 那 Cat 范畴之间的箭头，其实就是函子的函子， 又升维度了，我们有个特殊的名字给它，叫 喵的变换 {{{ruby(自然变换,Natural Transformations)}}} 。

#+CAPTION[Functor G η]: Functor F 和 G 以及 F 到 G 的自然变化

images/natrual-transformation.png

范畴 c 上的函子 f 到 g 的自然变化就可以表示成：

type Nat c f g = c (f a) (g a)

Scala 3 的 rank n types[fn:6] 也很简洁：

type Nat[C[_,_],F[_],G[_]] = [A] => C[F[A], G[A]]

如果换到 Hask 范畴上的自然变化就变成了：

type NatHask f g = f a -> g a
type Nat[F[_],G[_]] = [A] => F[A] => G[A]

这就是 Scala 中常见的 FunctionK[fn:15]。

恭喜你到达 Functor 范畴.

当然, 要成为范畴，还有两个属性:

  • id 为 f a 到 f a 的自然变换
  • 自然变换的组合

images/functor-category.png

别着急, 我们来梳理一下，如果已经不知道升了几个维度了，我们假设类型所在范畴是第一维度

  • 一维： Hask， 东西是类型，箭头是 ->
  • 二维： Cat， 东西是 Hask， 箭头是 Functor
  • 三维： Functor范畴， 东西是Functor， 箭头是自然变换

感觉到达三维已经是极限了，尼玛还有完没完了，每升一个维度还要起这么多装逼的名字，再升维度老子就画不出来了。

所以，是时候引入真正的技术了 – String Diagram。

String Diagram

String Diagram[fn:16] 的概念很简单，就是点变线线变点。

还记得当有了自然变换之后，三个维度已经没法表示了，那原来的点和线都升一维度，变成线和面，这样，就腾出一个点来表示自然变换了。

images/p1-string-diagram.png

组合（compose）的方向是从右往左，从下到上。

阅读起来，你会发现左右图给出的信息是完全等价的：

  1. 范畴 E 通过 函子 D 到范畴 D，范畴 D 通过函子 F 到范畴 C
  2. 范畴 E 通过 函子 E 到范畴 C
  3. F . G 通过自然变换 α 到 H

Adjunction Functor 伴随函子

伴随函子是范畴 C 和 D 之间有来有回的函子，为什么要介绍这个，因为它直接可以推出单子。

让我们来看看什么叫有来回。

images/p1-adjunction-functor.png

其中：

  • 图右：一个范畴 C 可以通过函子 G 到范畴 D，再通过函子 F 回到 C，那么 F 和 G 就是伴随函子。
  • 图中：范畴 C 通过函子组合 F . G 回到范畴 C，函子 G . F 通过自然变换 η 到函子 1_D
  • 图左：范畴 D 通过函子组合 G . F 回到范畴 D，函子 1_C 通过自然变化 ε 到函子 F . G

同时根据同构的定义，G 与 F 是 同构 的。

同构指的是若是有

f :: a -> b
f':: b -> a

那么 f 与 f’ 同构，因为 f . f' = id = f' . f

伴随函子的 F . G 组合是 C 范畴的 id 函子 F . G = 1_c

images/p1-ajunction-functor-compose.png

注意看坐标，该图横着组合表示函子组合，竖着是自然变换维度，因此是自然变换的组合。

images/p1-ajunction-functor-compose-nat.png

当组合两个自然变换 η . ε 得到一个弯弯曲曲的 F 到 F 的线时，我们可以拽着 F 的两端一拉，就得到了直的 F 线。

String Diagram 神奇的地方是所有线都可以拉上下两端，因为线不管是弯的还是直的，包含的信息并不会发生变化。 这个技巧非常有用，在之后的单子推导还需要用到。

从伴随函子到 {{{ruby(单子,Monad)}}}

有了伴随函子，很容易推出单子，让我们先来看看什么是单子：

  • 首先，它是一个自函子（endofunctor） T
  • 有一个从 i_c 到 T 的自然变化 η (eta)
  • 有一个从 T^2 到 T 的自然变化 μ (mu)

images/p1-monad-properties.png

class Endofunctor c t => Monad c t where
  eta :: c a (t a)
  mu  :: c (t (t a)) (t a)
trait Monad[C[_, _], T[_]]] extends Endofunctor[C, T]:
  def eta[A]: C[A, T[A]]
  def mu[A]: C[T[T[A]], T[A]]

同样，把 c = Hask 替换进去，就得到更类似我们 Haskell 中 Monad 的定义

class Endofunctor m => Monad m where
  eta :: a -> (m a)
  mu :: m m a -> m a
trait Monad[M[_]] extends Endofunctor[M]:
  def eta[A]: A => M[A]
  def mu[A]: M[M[A]] => M[A]

要推出单子的 η 变换，只需要让 FG = T。可以脑补一下，因为是自函子，因此可以抹掉 D， 想象一下，当 D 这一块面被拿掉之后，线 F 和线 G 是不是就贴在一起了呢？两根贴着的线，不就是一根线吗？

images/p1-ajunction-functor-to-monad-eta.png

同样的，当 FG = T, 也就是把 D 这陀给抹掉，F 和 G 就变成了 T。

images/p1-ajunction-functor-to-monad-mu.png

三角等式

三角等式是指 μ . T η = T = μ . η T

要推出三角等式只需要组合 F η G 和 ε F G

images/p1-adjunction-functor-triangle.png

images/p1-monad-triangle.png

换到代码上来说

(mu . eta) m = m

同样的，左右翻转也成立

images/p1-adjunction-functor-triangle-reverse.png

images/p1-monad-triangle-reverse.png T η 就是 fmap eta

(mu . fmap eta) m = m

如果把 mu . fmap 写成 >>= , 就有了

m >>= eta = m

结合律

单子另一大定律是结合律，让我们从伴随函子推起

假设我们现在有函子 F η G 和 函子 F η G F G, compose 起来会变成 F η G . F η G F G images/p1-ajunction-functor-monad-laws-1.png

用 F G = T ， F η G = μ 代换那么就得到了单子的 μ . μ T images/p1-ajunction-functor-monad-laws-2.png

当组合 F η G 和 F G F μ G 后，会得到一个镜像的图 images/p1-ajunction-functor-monad-laws-3.png

对应到单子的 μ . T μ

结合律是说 μ . μ T = μ . T μ , 即图左右翻转结果是相等的，为什么呢？看单子的String Diagram 不太好看出来，我们来看伴随函子

如果把左图的左边的 μ 往上挪一点，右边的 μ 往下挪一点，是不是跟右图就一样了 images/p1-ajunction-functor-monad-laws-4.png

结合律反映到代码中就是

mu . fmap mu = mu . mu

代码很难看出结合在哪里，因为正常的结合律应该是这样的 (1+2)+3 = 1+(2+3)，但是不想加法的维度不一样，这里说的是自然变换维度的结合，可以通过String Diagram 很清楚的看见结合的过程，即 μ 左边的两个T和先 μ 右边两个 T 是相等的。

Yoneda lemma / 米田共 米田引理

米田引理是说所有的函子 f a 一定存在两个变换 embed 和 unembed=，使得 =f a 和 (a -> b) -> F b 同构。

要再 Haskell 中做到这一波操作需要先打开 RankNTypes 的编译器开关：

{-# LANGUAGE RankNTypes #-}

embed :: Functor f => f a -> (forall b . (a -> b) -> f b)
embed x f = fmap f x

unembed :: Functor f => (forall b . (a -> b) -> f b) -> f a
unembed f = f id

Scala 3 不需要插件或者开关[fn:17]，如果是 Scala 2 可以用 apply 来模拟. 比如 Cats 中 FunctionK(~>)。

type ~>[F[_],G[_]] = [A] => F[A] => G[A]
def embed[F[_], A](fa: F[A])(using F: Functor[F]) =
  [B] => (fn: A=>B) => f.fmap(fn)(fa)
def unembed[F[_]](fn: [B] => (A => B) => F[B]): F[A] =
  fn(identity)

embed 可以把 f a 变成 (a -> b) -> f b

unembed 是反过来， (a -> b) -> f b 变成 f a

上个图可能就明白了：

images/yoneda-lemma.png

这个引理看似很巧妙，特别是用 id 的这个部分，但是有什么用呢？

如果着急可以跳到 {{{ruby(Free Monad,自由单子)}}} 部分，你会发现他是自由单子的基础。而且如果再往后会介绍的宇宙本原左看和右看，更会发现其中得精妙相似之处。

Rank N Type

前面说好的要解释 Rank N Type，这里赶快补充一下，不然等会我就忘了。

Haskell 中可以不用声明类型, 但是其实是省略掉 universally quantified forall, 如果把 forall 全部加回来, 就明了很多:

  • Monomorphic Rank 0 / 0级单态[fn:7]: t
  • Polymorphic Rank 1 / 1级 变态 多态: forall a b. a -> b
  • Polymorphic Rank 2 / 2级多态: forall c. (forall a b. a -> b) -> c
  • Polymorphic Rank 3 / 3级多态: forall d . (forall c . (forall a b . a -> b) -> c) -> d

看 rank 几只要数左边 forall 的个数就好了.

一级多态只锁定一次类型 a 和 b

二级多态可以分两次确定类型, 第一次确定 c, 第二次确定 a b

三级多台分三次: 第一次 d, 第二次 c, 第三次 a b

比如:

rank2 :: forall b c . b -> c -> (forall a. a -> a) -> (b, c)
rank2 b c f = (f b, f c)

rank2 True 'a' id
-- (True, 'a')
  • f 在 f True 时类型 Boolean -> Boolean 是符合 forall a. a->a 的
  • 与此同时 f 'a' 时类型确实是 Char -> Char 但也符合 forall a. a->a

看 Scala 的更简单，因为 Scala 不能省去 universally quantified，只需要数方括号即可。 最左边 [B, C] 是 rank1， fn 的类型里的 [A] 是 rank2。

def rank2[B, C](b: B, c: C)(fn: [A] => A => A): (B, C) =
  (fn(b), fn(c))

rank2(true, 'a')([A] => (a: A) => A)

如果不用rank2 而是只有 rank1 类型系统就懵逼了:

rank1 :: forall a b c . b -> c -> (a -> a) -> (b, c)
rank1 b c f = (f b, f c)
def rank1[A, B, C](b: B, c: C)(fn: A => A): (B, C) =
  (fn(b), fn(c))

f 在 f True 是确定 a 是 Boolean，在rank1多态是时就确定了 a -> a 的类型一定是 Boolean -> Boolean ， 然后当看到 f 'a' 时类型就挂了，因为 'a' 不是 Boolean 。

Kleisli Catergory

{{{ruby(函子,Functor)}}} 的范畴叫做 {{{ruby(函子范畴,Functor Catergory)}}}, 自然变换是其箭头。那{{{ruby(单子,Monad)}}}也可以定义一个范畴吗?[fn:8]

是的, 这个范畴名字叫做 +单子范畴+[fn:9] {{{ruby(可莱斯利范畴,Kleisli Catergory)}}}[fn:10]，那么 Kleisli 的箭头是什么？

images/kleisli.png

我们看定义，Kleisli Category：

  1. 箭头是 Kleisli 箭头 a -> T b
  2. 东西就是c范畴中的东西. 因为 a 和 b 都是 c 范畴上的， 由于T是自函子，所以 T b 也是 c 范畴的

看到图上的 {{{ruby(T f, fmap f)}}} 和 μ 了没？[fn:11]

f :: b -> T c
fmap f :: T b -> T T c
mu :: T T c -> T c
def f[T[_], B, C](b: B): T[C]
def fmap[T[_], B, C](f: B => C)(tb: T[B]): T[T[C]]
def mu[T[_], C](ttc: T[T[C]]): T[C]

紫色的箭头 T f=[fn:12] 和紫色的虚线箭头 \mu 连起来就是 =T f', 那么最出名的 bind >>= 符号终于出来了:

tb >>= f = (mu . fmap f) tb

Scala 中通常叫作 flatMap ，但如果你用 Cats 也是可以用 >>= 的。

def flatMap[T[_], B, C](f: B => T[C])(tb: T[B]): T[C] = (mu compose fmap(f))(tb)

下面这个大火箭 <=< 可以把蓝色箭头组合起来.

(f <=< g) = mu . T f . g = mu . fmap f . g
def <=<[T[_], A, B, C](f: B => T[C])(g: A => T[B]): A => T[C] =
  mu compose fmap(f) compose g

因此大火箭就是 Kleisli 范畴的 compose

(<=<) :: Monad T => (b -> T c) -> (a -> T b) -> (a -> T c)

Summary

第一部分理论部分都讲完了， 如果你读到这里还没有被这些{{{ruby(吊炸天,乱七八糟)}}}的概念劝退， 那么你这份如此强大得信念感，其实到后面两部分也不会有什么用。 因为，接下来的例子会很简单，我们要通过编程中常遇到的场景看看理论到底该如何得到实践？

Footnotes

[fn:17] https://blog.oyanglul.us/scala/dotty/rank-n-type

[fn:16] https://www.youtube.com/watch?v=kiXjcqxVogE&list=PL50ABC4792BD0A086&index=5

[fn:15] https://blog.oyanglul.us/scala/dotty/en/functionk

[fn:14] 为什么用两种语言呢？第一： 这样代码量会翻倍，可以凑篇幅字数。 这样大家会熟悉多种语言对同一概念的诠释，从而举一反三。 第二：读者受众会大一点，因为毕竟Haskell的表述比较简洁，有可能很容易理解，但是跟主流语言的表达方式大为不同，也有可能很难适应，加上表达方式更为具体的 Scala，便于加深理解。

[fn:13] 可以继续看第二部分，看完概念是如何在现实中实现的，再回来看一遍，会感觉好很多。

[fn:1] https://en.wikipedia.org/wiki/Cheshire_Cat

[fn:2] 如果没看就刚好不要看了, 确实有些误导

[fn:3] 等等, 写前端怎么了? JavaScript 只是我觉得顺手的若干语言之一, JS用户那么多, 写书当然要用 JS 啦, 难道用 Idris 那还能卖得掉吗? 当然最后用JS也没怎么卖掉…

[fn:4] 并不是说这两门语言一定在鄙视链顶端, 而是拥有强大类型系统的语言才能体现出范畴论的内容

[fn:5] 这里可以把 Functor 的第一第二个参数消掉, 因为已经知道是在 Hask 范畴了

[fn:6] https://blog.oyanglul.us/scala/dotty/en/rank-n-type 别急, 后面马上讲到

[fn:7] 也就不是不变态

[fn:8] 当然, 单子是自函子，所以也可以是自函子范畴

[fn:9] 怎么说也是函数式编程的核心,怎么可以叫的这么low这么直接

[fn:10] 这个是我瞎翻译的, 但是读出来就是这么个意思, 真的, 不骗你, 照这么读绝对装的一手好逼, 不会被嘲笑的

[fn:11] (敲黑板) 就是紫色那根嘛!

[fn:12] 即 fmap f