上一篇:自由幺半群编程
原文地址:https://bartoszmilewski.com/2...segmentfault
是时候谈谈集合了。数学家们对集合论是又爱又恨。它是数学中的汇编语言——至少它经常是。范畴论在某种程度上尝试跳出集合论,一个众所周知得事实就是不存在全部集合的集合,但全部集合的范畴,Set,是存在的。这就很好。另外一方面,咱们假定一个范畴中任意两个对象之间的态射构成一个集合。咱们还叫它hom集。为了公平,还有一种范畴论中态射并不构成集合。取而代之的是它们是另外一个范畴中的对象。这些范畴使用的不是hom集而是hom对象,它们被称做富范畴。然而,接下来,咱们还将只看那些使用可爱的原始形式的hom集的范畴。数据结构
富范畴的原文为enriched category,我没有找到它对应的中文。译者注。
集合是你能找到的最接近范畴对象的平凡的家伙了。一个集合有元素,但你不能对这些元素说更多的事。若是你有一个有限集,那么你能数出他们来。你能够用基数大体对无限集的元素计数。好比,天然数集小于实数集,即便它们都是无限多的。可是,可能有些让人惊讶的是,有理数集和天然数集同样大。ide
除此以外,全部有关集合的信息都能表如今它们之间的函数上——尤为是叫作同构的那些可逆的家伙。同构的集合在任何意义下都是彻底同样的。在我引发基础数学家们的愤怒以前,让我解释一下:相等和同构的区别具备很是根本的重要性。实际上它是数学最新的分支,同伦类型论(the Homotopy Type Theory ,HoTT)关心的主要问题之一。我提到HoTT是由于它是灵感来源于计算的一门纯粹的数学理论,而它主要的支持者之一,Vladimir Voevodsky,主要是在研究Coq定理证实辅助器时顿悟的。数学和编程的互动是双向的。函数
关于集合的重要的一课是,不想元素那样,集合是能够比较的。好比,咱们能够说一个给定的天然变换的集合同构于某个态射的集合,由于一个集合就只是一个集合。在这个例子里同构就只是说对于一个集合里的每一个天然变换另外一个集合里都有惟一的一个态射与之对应,反之亦然。他们能够互相配对。若是苹果和橘子是不一样的范畴里的对象,那你不能比较苹果和橘子,但你能够比较苹果的集合和橘子的集合。一般把一个范畴问题转换成一个集合论的问题会给咱们一些必要的直观或者甚至让咱们证实有价值的定理。post
每一个范畴都天生具备一个到Set的典型映射族。这些映射其实是函子,因此它们维持范畴的结构。让咱们构造一个这样的映射。性能
咱们固定C的一个对象a
而后选择另外一个对象x
,hom集C(a, x)
是个集合,也就是Set的一个对象。当咱们保持a
固定不变而变化x
时,C(a, x)
也会在Set中变更。所以咱们有了个从a
到Set的映射。spa
若是咱们想强调咱们正把hom集看做以它的第二个参数做自变量的映射,就使用记号:翻译
C(a, -)
其中链接号充当了该参数的占位符。3d
对象的映射能够容易地拓展到态射的映射。咱们取C中两个任意对象x
和y
的态射f
。在咱们刚刚定义的映射下,对象x
被映为集合C(a, x)
而y
被映为C(a, y)
。若是该映射要成为一个函子,f
必须被映为这两个集合之间的一个函数:
C(a, x) -> C(a, y)
让咱们逐点定义这个函数,逐点就是分别对每一个取值分别处理。这里咱们应该选取C(a, x)
中的一个任意元素——咱们叫它h
好了。首尾相连的态射是可复合的。h
的尾和f
的头就是这种匹配的状况,因此它们的复合:
f ∘ h :: a -> y
是一个a
到y
的态射。所以它是C(a, y)
的一个家伙。
咱们刚刚找到了从C(a, x)
到C(a, y)
的函数,它是f
的像。若是不至于引发歧义,咱们把这个提高后的函数写做:
C(a, f)
它在态射h
上的行为是:
C(a, f) h = f ∘ h
因为在任意范畴里均可以这样构造,它确定也能够在Haskell类型范畴中实现,这个hom函子就是众所周知的Reader
函子:
type Reader a x = a -> x
instance Functor (Reader a) where fmap f h = h . h
如今咱们考虑一下,若是把固定hom集的源点改成固定靶点,会发生什么。换句话说,咱们问是否映射
C(-, a)
也是个函子。它是,但它再也不是协变的,它是逆变的。这是由于一样的首尾相连的态射的配对会致使f
后复合而不是C(a, -)
的那种前复合。
前复合对应的英文为precomposition,后复合对应的英文为postcomposition,f
前复合就是说复合时f
在前,f
后复合就是说复合时f
在后。
咱们已经看到了Haskell中的这个逆变函子。咱们叫它Op
:
type Op a x = x -> a
instance Contravariant (Op a) where contramap f h = h . f
最后,若是咱们让两个对象均可变,就获得了逆变协变函子(profunctor)C(-, =)
,它的第一个参数是逆变的,第二个参数是协变的(为了强调两个参数能够独立地变化,咱们用双链接号做为第二个占位符)。咱们以前已经看过这个逆变协变函子了,是在咱们讲到函子性的时候:
instance Profunctor (->) where dimap ab cd bc = cd . bc . ab lmap = flip (.) rmap = (.)
在第一部分的翻译中,profunctor被译为“副函子”,我认为不妥,因而找到了逆变协变函子这样的叫法。译者注。
重要的教训是这个观察在任意范畴都成立:把对象映为hom集是具备函子性的。既然逆变性等价于一个反范畴的映射,咱们就能够把这件事简写为:
C(-, =) :: C^op x C -> Set
咱们已经看到,选择C中的每个对象a
,咱们得到一个从C到Set的函子。这种指向Set的结构保持的映射一般被称为一个表示。咱们把C中的对象和态射表示为Set的集合和函数。
函子C(a, -)
自己一般说是可表的。更通常地,任意与选择了某个a
的hom函子天然同构的函子F
被称做可表的。这种函子必定是指向Set的,由于C(a, -)
指向Set。
我以前说过咱们常常把同构当作同一的。更通常地,咱们把一个范畴中同构的对象看做同一的。这是由于对象除了到其余对象(和他们本身)的态射关系外没有其余的结构了。
好比说,咱们以前谈到过幺半群范畴,Mon,它最开始就是用集合建模的。可是咱们很当心地选取了那些保持了集合的幺半群结构的函数做为态射。因此若是Mon的两个对象是同构的,意味着它们之间有一个可逆的态射。它们精确地具备相同的结构。若是咱们看看这些态射所基于的集合和函数,咱们将会看到一个幺半群的单位元被映射到了另外一个的单位元,而且两个元素的积被映射为它们的像的积。
一样的推断能够用在函子上。两个范畴间的全部函子构成了一个范畴,而天然变换扮演了态射的角色。因此若是在两个函子间存在可逆的天然变换,那么它们是同构的,而且可以被视为同一的。
让咱们从这种视角分析一下可表函子的定义。由于F
是可表的,咱们须要:有C中的一个对象a
;一个从C(a, -)
到F
的天然变换α
;另外一个反过来的天然变换β
;而且它们的复合是恒等天然变换。
让咱们看看α
在某个对象x
上的份量。这是一个Set中的函数:
α_x :: C(a, x) -> F x
这个变换的天然性条件告诉咱们,对于任意从x
到y
的态射f
,下面的四方图是交换的:
F f ∘ α_x = α_y ∘ C(a, f)
在Haskell中,咱们能够用多态函数代替天然变换:
alpha :: forall x. (a -> x) -> F x
其中有可选的forall
量词。因为参数化多态(这是一个我以前提到的免费定理的一个),天然性条件
fmap f . alpha = alpha . fmap f
会自动知足。注意,左式的fmap
是定义在函子F
上的,而右边的那个是定义在reader函子上的。由于reader的fmap
就只是作了函数前复合,咱们甚至能够再精确些。做用在C(a, x)
的一个元素h
上时,天然性条件简化为:
fmap f (alpha h) = alpha (f . h)
另外一个变换β
是反方向走的:
beta :: forall x. F x -> (a -> x)
它必须遵照天然性条件,而且它必须是α
的逆:
α ∘ β = id = β ∘ α
咱们以后将会看到从C(a, -)
到任意指向Set的函子的天然变换总会存在(米田引理),但它不必定可逆。
让我给你个Haskell的例子吧——列表函子而且用Int
做为a
。这里是能实现这件事的一个天然变换:
alpha :: forall x. (Int -> x) -> [x] alpha h = map h [12]
我任取了数字12而且用它建立了个单例列表。接着我就能在这个列表上fmap
函数h
获得一个h
返回值类型的列表。(实际上这种变换的数目和整数列表的数目同样多。)
天然性条件就等价于map
(fmap
的列表版本)的可复合性:
map f (map h [12]) = map (f . h) [12]
可是要是咱们试图寻找逆变换,咱们不得不把任意类型x
的列表变成一个返回x
的函数:
beta :: forall x. [x] -> (Int -> x)
你可能会考虑从列表中检索出一个x
,好比,用head
,但它不能应用在空列表上。注意没有哪一个a
的选择(以代替Int
)可让它工做。因此列表函子并非可表的。
还记得咱们说过Haskell函子有点像容器吗?一样地咱们能够把可表函子看做把函数调用(hom集的成员在Haskell中仅仅就是函数)后的忆存结果存储起来的容器。表示对象,也就是C(a, -)
里的类型a
被看做关键字类型,用它咱们能够获得一个函数的表值。咱们所称做α
的变换叫tabulate
,它的逆,β
,叫index
。这是一个(略微简化的)Representable
类的定义:
class Representable f where type Rep f :: * tabulate :: (Rep f -> x) -> f x index :: f x -> Rep f -> x
忆存一词英文为"memoize",我没有找到相应的中文。它专指计算机领域将函数的运行结果保存下来,下次调用时直接取出而不从新计算的加速方法。
注意表示类型,也就是咱们的a
,这里被叫作Rep f
,是Representable
定义的一部分。星号只是说Rep f
是个类型(而不是类型构造子,或者其余更奇怪的)
无限列表,或者叫流,是不能够为空的,它是可表的。
data Stream x = Cons x (Stream x)
你能够把他们当作一个接受Integer
参数的函数的忆存值。(严格地讲,我应当用非负天然数,但我不想让个人代码更复杂。)
为了tabulate
这样一个函数,你得创造一个值的无限流。固然,这能作到仅仅是由于Haskell是惰性的。值只有在须要时才被求值。你能够用index
获得忆存值。
instance Representable Stream where type Rep Stream = Integer tabulate f = Cons (f 0) (tabulate (f . (+1))) index (Cons b bs) n = if n == 0 then b else index bs (n-1)
这颇有趣,你能够只实现一个忆存表就覆盖任意返回类型的函数的族。
逆变函子的可表性也是相似定义的,只不过咱们固定了C(-, a)
的第二个参数。或者等价地说,咱们能够考虑从C_op
到Set的函子,由于C_op(a, -)
就是C(-, a)
。
可表性有个有趣的变形。回忆hom集能够在笛卡尔闭范畴里被当作指数对象。hom集C(a, x)
就等价于x_a
,而且一个可表函子F
咱们能够写成:
-_a = F
让咱们两边取对数,这只是随便看看:
a = log F
固然,这只是个纯粹的公式变换,但若是你知道些对数的性质,那就会颇有用了。尤为是,能够证实做用于积类型的函子能够表示成和类型,而和类型的函子并不都是可表的(例子:列表函子)。
最后,注意到一个可表函子给咱们提供了一样一件事情的两种不一样实现——一种是函数,一种是数据结构。它们有着彻底相同的内容——一样的值会被一样的关键字检索到。这就是我以前谈到的“同一”的意思。只要两个天然同构的函子所涉及的内容是是同一的,那它们就是同一的。另外一方面,这两种表示方式常常会用不一样方式实现所以可能有彻底不一样的性能。忆存被用来提高性能因此可能使运行时间大大缩减。在实践中,能对相同的隐性计算过程创造不一样的表达方式是很是有价值的。因此,很让人惊喜的是,即便如今并无关心性能,范畴论也为探索其余可能的有实际价值的实现提供了足够的机会。
Maybe
不是可表的。Reader
函子可表吗?Stream
的表示,忆存平方函数。Stream
的tabulate
和index
确实是互逆的。(提示:使用概括法)函子:
Pair a = Pair a a
是可表的。你能不能猜到表示它的类型是什么?实现tabulate
和index
。
感谢Gershom Bazerman检查个人数学和逻辑,以及André van Meulebrouck在整个系列中的编辑上的帮助。
下一篇:米田引理