预备知识-Cats和Cats

事实证明,非洲人在任何地方都非。搞不定论文的我只能接着写一些没用的。预定的计划是结合Cats以及常见的猫论的内容。自己也是个半吊子,写出来总结一下。

从Cats开始

Category是一个简单抽象的概念。简单来说一个Category\(C\)包含两种元素:

  • 一堆object \(ob(C)\)
  • 一堆morphisms \(hom(C)\)。所谓morphism,是从source object映射到target object的箭头(arrow)。当然,这里的object应该属于\(ob(C)\)。我们可以写作\(f: a \rightarrow b\)或者\(hom(a, b)\)。此外,还要满足一个性质,对于objects a, b以及c,如果有\(f: a \rightarrow b\)以及\(g: b \rightarrow c\),则必须要有一个arrow\(a \rightarrow c\)。可以写成\(g \circ f\)称为g after f

此外,还应该满足两条公理。

  • associativity。 对于\(f: a \rightarrow b\)\(g: b \rightarrow c\)以及\(h: c \rightarrow d\)。则应该有\(h\circ (g \circ f) = (h \circ g) \circ f\)
  • identity。 对于每一个object x,都应该存在morphism\(id_x: x -> x\),被称为\(x\)identity morphism。由于这个性质,对于\(f\)应该有\(f \circ id_A = f\)

所以,对于category,我们可以想象成一堆圈,以及把他们连接起来的箭头。

Category

Category

Types and Cats

Category中一个重要的性质就是morphisms的组合。但并不是任意两个morphisms都可以组合,他需要前一个morphismtarget object是后一个morphismsource object,而这一点和我们在编程中的函数很相似。

Types 到 Hask

一种对于Type最直观的解释就是一个type就是代表一堆value的集合(set)。Set中的元素可以是有限的,比如Bool就是{true, false},也可以是无限的,比如String

我们先来看定义在Set上的范畴Set(之后我们都用这种粗体代表一个特定的范畴)。在Set中,object是一个个set,而morphisms就是functions。因此,如果我们认为type其实就是一种set的话,其实我们可以在类型上也定义一个范畴。但是对于morphism和函数,这里要求编程语言中的函数和数学上的函数一致,即没有副作用并且可以在有限步内结束。没有副作用好说,但是函数能不能在有限步之内结束这个停机问题却没法解决。为此我们引入一个新类型\(\bot\),它用来代表没有返回类型(比如抛异常)。值得一提的是,\(\bot\)并不是常见的void,在Scala中更像是NothingHaskell中的Empty。最终,我们把包含\(\bot\)的所有类型的范畴(其实并不是范畴,不过可以在某些程度上看成范畴,具体的可以看引用3)称为Hask

Monoid

相比其他的M wordsMonoid是一个相对好理解的例子。

集合中的Monoid

中文称Monoid为幺半群,即包含幺元的半群。半群说明他包含一个二元运算\(*\),使得所有的\(a, b \in S\),都有\(a * b \in S\),而且\(*\)满足结合律。同时他还存在幺元,即存在\(e\)满足\(e *a = a * e = a\)

很明显自然数在加法上是一个MonoidString以及连接操作满足Monoid

Cats中的Monoid

Cats上的Monoid有一些不同,我们要定义的是objectmorphism。其中objects肯定还是其中的元素,但是集合中的二元操作就要稍作变化,对于一个二元操作可以看成\(f: a \rightarrow b \rightarrow c\),为了让它可以映射object,对于每一个\(f\),我们都可以先给他一个参数\(a\)让他变成\(f : b \rightarrow c\)。写成代码就可以当成

1
2
def op(a: A): C = 
(x: B) => biop(a, x)

举个例子,对于正数和加法。我们就不能用+来当做 morphism,而要用+1, +2这种来当做morphism,并且还有+0来当做identity

Monoid是个很常见的例子,我们之后还会再提到它。

Objects in Cats

Cats中有一些特殊的objects

Isomorphism for objects

先介绍isomorphismisomorphism是一个存在很广泛的概念,最直观的感觉就是两个东西如果是isomorphism的那么他们具有相似的形状。正式一点,对于一个范畴C中,存在\(f: A \rightarrow B\)以及一个\(g: B \rightarrow A\)满足

\[g \circ f = id_A\ \ and\ \ f \circ g = id_B \]

换而言之,\(g = f^{-1}\),我们就说A is isomorphic to B

Initial Object

Initial object\(I\)指的是对于范畴C中的任意object \(A\),都有且只有一个arrow满足\(f: I \rightarrow A\)。比如下面这个例子

initial

initial

对于我们之前Hask,我们可以拥有函数absurd:: Empty -> r,把Empty映射到任意类型,所以这里Empty就是我们的initial object

Terminal Object

类似的,terminal object\(T\)是指对于范畴C中的任意object\(A\),有且只有一个arrow满足\(f: A \rightarrow T\)。就像

Terminal

Terminal

同样在Hask,我们有函数unit:: a -> (),使得()称为terminal object。为什么其他类型不行呢?因为其他类型都至少有两个及其以上的值。这样对于一个函数

1
2
3
toBool :: a -> Bool
toBool _ = true
toBool _ = false

有两个不同的function,能将一个类型映射到Bool上。而只有一个元素的类型应该是同构与()的。对于Initial object也是这个道理。

Duality

对偶也是个很直观的概念,你可以想象成把一个范畴中所有的箭头都反过来。对于C,我们称其对偶为\(\textbf{C}^{op}\)。比如,如果范畴__C__里面有\(f: A \rightarrow B\)以及\(g: B \rightarrow C\),然后组合得到\(h: A \rightarrow C\),那么\(\textbf{C}^{op}\)里面就应该有\(f^{op}: B \rightarrow A\)以及\(g^{op}: C \rightarrow B\),组合得到\(h^{op}: C \rightarrow A\)

Duality

Duality

Product and Coproduct

Products

Setproduct我们都见过,称为cartesian product,即

\[A \times B = \{(a, b)| a \in A, b \in B\}\]

现在这里存在两个投影

product

product

类似的,我们定义objectproductobject aobject bproductobject c,意味着object c以及其两个projections,对于任意的object \(c\prime\)以及它的两个projections都有唯一的morphism m\(c\prime\)\(c\)可以factorizes(分解)\(c\prime\)的两个projections

这一段话可能有点别扭,我们先看一个例子。

对于(Int, Bool)这个IntBool两个typeproduct。我们可以构造

1
2
def fst(t: (Int, Boolean)) = t._1
def snd(t: (Int, Boolean)) = t._2

显然我们依旧有其他的类型可以构造这种形式,比如(Int, Double, Bool)

1
2
def p(t: (Int, Double, Boolean)) = t._1
def q(t: (Int, Double, Boolean)) = t._3

但是为什么后者不是product呢,原因也很简单他能被分解,我们可以构造

1
def m(t: (Int, Double, Boolean)) = (t._1, t._3)

很显然,我们可以重新得到

1
def m(t: (Int, Double, Boolean)) = (p(t), q(t))

Coproduct

Coproduct就是和Product就是对偶的关系。我们定义object aobject bCoproductobject c,意味着object c以及其两个projections,对于任意的object \(c\prime\)以及它的两个projections都有唯一的morphism m\(c\)\(c\prime\)可以factorizes(分解)\(c\prime\)的两个projections

这一段话基本和Product一样,不同之后最后\(c\)\(c\prime\)是反过来的。先看看这个图。我们常见的一个例子就是,Either Int BooleanBooleanInt

1
2
def p(i: Int) = Left(i)
def q(i: Boolean) = Right(i)
coproduct

coproduct

Algebra of Types

之前也写过关于Algebra Types,这里其实也很容易发现Product其实是Product Types,而Coproduct其实是Sum Types

我们继续换个角度。在HaskellEither是这么定义的

1
Either a b = Left a | Right b

可以看做a + b的话,然后把(a, b)看做乘法,那么对于List

1
List a = Nil | Cons a (List a)

就变成

$x = 1 + a + a * a + a * a * a + … $

它由无限长的加法和乘法构成。我们确实拥有了一个Algebra

代数

代数

对应到一阶逻辑上。

逻辑

逻辑

再进一步就是Curry-Howard isomorphism,我们之后再谈。

引用

  1. Category in wikipedia
  2. Monoid in wikipedia
  3. Hask
  4. Category Theory for Programmers
  5. Category Theory (Oxford Logic Guides)