一点尾巴以及-Cats和Cats

差点3月份就没有产出了,毕业论文算是刚刚编出来,虽然不知道能不能顺利毕业。这次内容有很水,最近又搞起来炼丹,烂七八糟什么事情都有。开始实习,马上又要放清明了。

Exponentials

internal hom-set

一个类型其实就是一堆值的集合。对于Boolean就是元素只有truefalse两个元素的集合。而对于一个类型为a->b的函数,就是出于两个object之间的morphism,而morphism构成的集合叫hom-set。而从另一个角度看a->b也是一个类型我们也可以构造诸如(a->b)->(a->c)来把a->b这个函数看做一个object。这样其实hom-set的内容其实依旧是object集合中的一部分。所以这部分对象叫internal hom-set

Exponentials

我们之前提过sum types以及product types。而这种function object样子的internal hom-set,他们好像并不是上述类型。比如Char -> BooleanCharASCII表示共256个元素,Boolean共2个元素,那么Char->Boolean应该有\(2^{256}\)即对于Char中的每一个元素都能选择映射到Boolean中任意一个元素中。因此internal hom-setab,就可以称为exponential\(b^a\)表示。

Cartesian Closed Categories

一个cartesian closed category必须存在:

  1. termainal object
  2. 对于任意objects pairproduct
  3. 对于认为objects pairexponential

一个cartesian closed category可以看成一个允许无穷序列乘的代数。而terminal object就是其中的0元。

Algebraic Data Types的一些性质

有了加法和乘法以及0、1元,我们可以讨论一下具体的性质。

我们利用initial object代替0,用final object代替1,而指数是internal hom-object。对于Hask,我们使用Void来当做0,而1(),而指数就是function type。这样\(a^0 = 1\)的就是Void -> a,这其实就是absurd。实际上并没有这种函数,而且所有的Void -> a其实都是一样的,因为它根本就不会正常运行,不会返回结果。

同理,\(1^a = 1\)就变成了a -> ()。而\(a^1 = a\)就变成了() -> a

接下来看一些更复杂的例子,对于\(a^{b + c} = a^b + a^c\)

1
f: Either Int Double -> String

这种样子,可以通过下面这种方式定义

1
2
f (Left n) = if n < 0 then "" else ""
f (Right x) = if n < 0.0 then "" else ""

然后\((a \times b)^c = a^c \times b^c\)可以理解成

1
f: String -> (Double, Int)

等价于

1
2
3
4
5
g1: String -> Double
g2: String -> Int

f: String -> (Double, Int)
f s = (g1 s, g2 s)

Curry-Howard Isomorphism

Curry-Howard Isomorphism是个很重要的概念,直观的来说它指出了逻辑推理和程序语言之间的一致性。程序语言与逻辑推理同构,程序类型与逻辑命题同构。在与外界隔离的情况下,一段程序等价于一段逻辑证明。

也是基于这些前提,才有很多用于逻辑证明的语言比如CoqAgdaF*等语言的出现。

Natural Transformations

functor将一个category映射到另一个category。虽然可能将多个object映射到同一个object,但是它不会破坏之前的形状。可以将source category看做target category的一个blueprint。可能存在多个functor将一个source category映射到多个target category,同时保留相同的形状。

假设存在CD两个范畴,对于C中的a,存在FG两个functora映射到F aG a。又因为F aG a同时存在于一个范畴,我们更倾向于直接使用D的中的箭头来连接F aG a。因此,我们natural的使用已经存在的连接。对于任意的object a,一个natural transformation就是一系列的F a映射到G amorphism

形式化定义

对于范畴CD之间的functor``FG,一个natural transformation\(\eta\)FG是指一系列的morphism满足如下性质

  1. natural transformation对于C中的对象amorphism\(\eta_x = F(X) \rightarrow G(X)\)。其中\(\eta_x\)被称为\(\eta\)X上的componet
  2. Component对于每一个morphism在C中的\(f: X \rightarrow Y\),都满足\(\eta_Y \circ F(f) = G(f) \circ \eta_X\)

如果我们多选几个object就可以有如下图的结构

根据这个图形,我们又可以得到更多的路径比如

\[G f \circ \eta_a = \eta_b \circ F f\]

换个角度,从一个容器的角度看待natural transformation。它把对一个object映射到morphism,同时还可以看成将一个morphism映射到commuting squares

Polymorphic Functions

有一个很常见的函数

1
2
3
4
def headOption[T](list: List[T]): Option[T] = list match {
case a::b => Some(a)
case _ => None
}

因为这个函数对于任意的T类型都成立,所以也被称为Polymorphic Functions。也是natural transformation

因此,我们可以得到一个functor的范畴,而其中的morphism就是natural transformation

然后我们整理一下思路。首先我们有范畴(为了区别之后的范畴以后就称为小范畴),范畴包含一堆objects以及morphisms。然后我们还有Cat,更高级一点的范畴,以functormorphism,以小范畴objects的范畴。再进一步,我们依然可以将functor看做objects,然后用natural transformation当做morphism。我们用Cat(C,D)表示范畴C和D之间的functor的集合。而一个functor的范畴[C,D]同时也可以看做两个范畴之间functor的集合。

2-Categories

一个Cat可以看做2-category,如果其满足

  1. 其元素是范畴。
  2. 1-morphisms为这些范畴中的functors
  3. 2-morphisms位functors上的natural transformations

对于一般的范畴C和D我们定义Hom-Category,即函子范畴\(D^C\)。这个和上面的指数类型很相似。

我们看一个例子

假如我们有两个functor

1
2
F :: C -> D
G :: D -> E

因此我们可以组合他们

1
G . F :: C -> E

假如我们有两个natural transformations分别为\(\alpha\)\(\beta\)。 然后作用于FG上。

1
2
a :: F -> F'
b :: G -> G'

这里我们并不能组合\(\alpha\)\(\beta\)。但是可以组合F'G'。因此,我们可以定义natural transformationhorizontal composition

\[ \beta \circ \alpha :: G \circ F -> G' \circ F' \]

这个结果也不难得到。我们看一个完整的图