Haskell/范畴论
本文将概述 Haskell 里应用的一个概念,范畴论。因此 Haskell 代码的展示将会伴随其对应的数学定义,为了让读者可以直观地理解范畴论的概念以及它与 Haskell 的关系,这种对应可能不那么绝对的严谨。
范畴论是什么
编辑范畴,本质上是一个简单的集合,包括三个组成元素:
- 对象.
- 态射,每个态射将两个对象(源对象和目标对象)连接在一起(它们有时被称为箭头(arrows),但本文避免使用该术语,因为它在 Haskell 中具有其他涵义。)如果 f 是源对象 A 到目标对象 B 的态射,写作 。
- 态射组合。例如:态射 和 态射 可以组合为态射 。
许多东西都可以称为范畴。例如,所有集合构成了范畴 Set,其态射为集合间的函数,而态射组合则为一般的函数复合(标粗的为范畴名)。全部的群构成了范畴 Grp,保持群结构的函数就是它的态射(群同态),比如任意两个群 G 和 H ,G 的操作符为 * ,H 的操作符是 · ,那么函数 只要满足如下条件就是一个态射:
这么看来貌似态射就是函数,但是事实并非如此。例如,任何偏序结构 (P,
) 都构成范畴,P 中的元素构成了该范畴的对象,任意两个元素 a 和 b 只要满足 a b ,那么存在态射 a \to b。另外,在相同的源对象和目的对象之间可以存在多个态射;以 Set 范畴为例, 和 都是从源对象 (实数集) 到目标对象 的函数,但是它们是不同的态射。
范畴公理
编辑范畴需要符合三条定律。第一条,也是最简单的一条,态射的组合操作需要满足结合律。
态射在 Haskell 中从右到左执行,因此使用 时,g 先执行,然后 f。
第二条,态射在组合操作下是闭合的。因此,如果存在态射 和 ,那么范畴 中一定会存在态射 。以下面范畴为例。
f 和 g 都是态射,所以我们一定能够通过组合他们在范畴中得到另一个态射。 那么哪一个是态射 呢?唯一可能的答案就是 。同样,我们可以得到 。
最后一条,在一个范畴 C 中,每一个对象 A 都会有一个单位态射, ,这个态射是组合操作的单位元。准确的说对于每一个态射 :存在
请注意,涉及组合操作的表达式 可以彼此相等,但各个态射不能相等。例如有两个态射从对象 A 到对象 B,即 和 ,表达式 相同,但态射 永远为假。
Hask,Haskell 范畴
编辑本节我们主要讨论范畴 Hask,其对象为 Haskell 中的类型,态射为 Haskell 中的函数,态射组合操作为 (·)
,在 Hask 中函数 f :: A -> B
为类型 A
到 B
的态射。范畴第一第二定律很容易验证,我们知道 (·)
是一个组合操作,显然,对于任何 f
和 g
,f . g
是一个新的函数。在 Hask 中,单位态射是 id
,所以很容易验证第三定律:id . f = f . id = f
[1]上面的定律并不是一个十分准确的转换,因为我们忽略了下标。在 Haskell 中函数 id
是 多态的 — 它的域和范围可以采用许多不同的类型,用范畴的概念解释就是可以存在许多不同的源对象和目标对象。但是范畴论中的态射是定义为 单态的 — 每个态射都有一个特定的源对象和一个特定的目标对象(注意:这里的 单态 不在范畴论上使用)。多态 Haskell 函数可以通过指定其类型(用单态类型 实例化)来实现单态,因此我们说 Hask 上类型 A
的单位态射是 (id :: A -> A)
会更精确。考虑到这一点,上述定律将被重新书写为:
(id :: B -> B) . f = f . (id :: A -> A) = f
但是为简单起见,当含义明确时,我们将忽略这种区别。
练习 |
---|
|
函子
编辑所以我们有了一些范畴,其包含对象以及将这些对象联系在一起的态射。下一个在范畴论中非常重要的概念是functor,他们将范畴联系在了一起。functor 的实质是范畴之间的转换关系,因此对于范畴 C 和 D,有 functor :
- 映射范畴 C 中任一对象 A 到范畴 D 中的对象 。
- 映射范畴 C 中任一态射 到范畴 D 中态射 。
// 未翻译完
- ↑ Actually, there is a subtlety here: because
(.)
is a lazy function, iff
isundefined
, we have thatid . f = \_ -> ⊥
. Now, while this may seem equivalent to⊥
for all intents and purposes, you can actually tell them apart using the strictifying functionseq
, meaning that the last category law is broken. We can define a new strict composition function,f .! g = ((.) $! f) $! g
, that makes Hask a category. We proceed by using the normal(.)
, though, and attribute any discrepancies to the fact thatseq
breaks an awful lot of the nice language properties anyway.