单子(Monad)是什么?单子是一种抽象,最早起源于范畴论,后来在计算机科学中也出现了它的身影(严格来说,因为在计算机科学中多个自由变量的情况更加常见,所以编程中的单子实际上是范畴论中的强单子)。单子在计算机科学中扮演着重要角色,特别是对于函数式编程。程序员可以利用单子将函数序列连接,对副作用和流、日志等进行抽象。除此之外,范畴论中的其它概念,如函子,也为异常处理和异步操作等提供了方案。范畴论的很多概念对函数式编程影响深远,学习一些范畴论的知识可以使我们更好地了解函数式编程。不过,直面范畴论是非此抽象的,如果了解过一些抽象代数(和代数拓扑)的知识再来学习,就不是非常困难了。
本文将从范畴论的角度解释Haskell(一门纯函数式编程语言)中的各种结构,更偏向于理论。网络上有不少文章利用盒子等物件来解释这些概念,然后引入范畴论,这样从具体到抽象符合人类的认知过程,确实不错,但是很多作者对于范畴论的(错误)解释容易把读者引入歧途,为学习范畴论的其他概念造成障碍。因此本文将以严格的数学定义展开描述,但是不必担心,我会给出很多例子来帮助大家理解的。
读者最好有一定的Haskell语言基础,至少有一定编程基础(对于不会编程的读者,本文的数学内容也是值得阅读的)。本文的首要目的是为了使读者更好地理解函数式编程的代数结构与范畴论的联系,而不是学习语言本身,因而本文更多时候给出的是数学公式和伪代码,只需理解即可(读者也可以使用自己擅长的编程语言实现可运行的实例)。
在开始学习范畴论之前,先来看看群论(Group Theory)
群论
抽象代数是一门研究各种代数结构(比如群、环、域、模、向量空间、格与域代数)的学科。在集合论中,我们通过函数来研究集合之间的关系。而在抽象代数中,我们利用态射研究代数结构之间的关系,而范畴论则是将一切都抽象了,研究不同对象和不同范畴之间关系。其中研究群的学科叫做群论,本文只需要了解一点简单的群论基础知识。
原群,半群,幺半群
群论的基本结构是群,但本文不研究它,我们只关注一些更基础的结构。先来看看原群(Magma)的定义:
一个原群由一个二元运算和一个集合 构成,在该二元运算下该集合是封闭的,也就是说:
-
元素为Boolean的集合B和AND运算构成一个原群 -
整数和加法运算构成了一个原群(实际上对于实数,有理数和自然数都是成立的)
如果一个原群还满足以下条件(结合律),则称它为一个半群
-
元素为列表(List)的集合L和连接运算++构成一个半群
如果一个半群还满足以下条件(单位元),则称它为一个幺半群(Monoid)(因为单位元也称幺元)
-
由集合构成的集合和并集运算构成一个幺半群,单位元是空集 -
整数和加法运算构成了一个幺半群,单位元是0(如果是乘法运算,则单位元是1)
再添加条件,我们还可以得到群,环,域等代数结构,不过这和我们的主题关系不大。群论的内容也就到此为止了,现在我们进入Haskell的世界。
Haskell 语言
Haskell是一门纯函数式编程(Pure functional programming)语言,更多地被用在计算机科研领域。即使读者学习过编程,也大概率没有了解过它。没关系,函数式编程非常友好,要掌握它的语法还是很简单的,即使没有编程基础也可以轻松掌握。具体语法将在下文的各个例子中解释。
Haskell中的幺半群
Monoid类型类
根据上面幺半群的数学定义,我们可以在Haskell中定义它的类型类:
class Monoid a where
mempty :: a
-- ^ Identity
mappend :: a -> a -> a
-- ^ Associative operator
-
class 定义了一个类型类(Type class),随后的Monoid是该类型类的名称。a代表泛型。 -
where 是固定要写的,后面跟着的内容是该类型类的约束规则(如果要将一个类型a作为Monoid的实例,必须实现这几条规则) -
var :: a 是类型为a变量var -
a -> b 是类型a到类型b的函数 -
此处的mempty就是单位元,mappend是运算。这就定义了一个幺半群。
上面提到,元素为列表(List)的集合和连接运算(++)构成一个半群,很显然空列表[]是它的单位元,因此它也是个幺半群,用haskell代码描述便是(幺半群公理并未在代码中体现,需要程序员自己保证):
instance Monoid [a] where
mempty = []
mappend = (++)
-
instance Typeclass a where
可以为类型a实现Monoid类型类。 -
[a]是一个列表,元素的类型为a -
[a]其实可以称为a的自由幺半群(Free monoid)(在抽象代数里,于一集合A上的自由幺半群是指一个幺半群,其元素都是由A内零个或多个元素以连接为二元运算而形成的有限序列)
Monoid同态
在抽象代数中,同态(homomorphism)是两个代数结构间保持结构不变的映射。现在我们只考虑幺半群。
设有一个函数满足以下条件:
则称函数是和之间的同态
-
设代表列表的集合,代表自然数的集合(包括0),则函数是到之间的同态,因为它显然满足:
length [] = 0
length (xs ++ ys) = length xs + length ys
范畴论
数学家能找到定理之间的相似之处,优秀的数学家能看到证明之间的相似之处,卓越的数学家能察觉到数学理论之间的相似之处,而最顶级的数学家能俯瞰这些相似之处之间的相似之处。
-- Stefan Banach
通过寻找各种代数结构的相似之处,抽象代数这门学科逐渐被建立起来。同态描述的是代数结构之间的相似性,同态本身又是一种态射。很多抽象的数学结构之间都有着相似之处,可以将他们抽象为态射,而范畴论(Category theory)就是利用态射研究相似之处之间的相似之处(当然这并不是终点,往上还有无穷范畴)。
范畴论的主要研究对象是范畴,数学家希望这个概念能够涵盖大量数学对象,足够广泛和抽象,所以不得不牺牲很多细节,只利用态射和对象来描述一个范畴。
范畴(Category)
范畴(Category)的定义并不依赖复杂的数学知识,它的结构是十分自然的:
一个范畴由以下三个部分构成:
一个类,其元素称为对象(Object)
一个类,其元素称为态射(Morphism)。每个态射 都只有一个源对象 及一个目标对象 ,且。称之为“从a至b的态射”,记为
一个二元运算,称为态射复合,使得对任意三个对象,有,态射和的复合写作或,态射满足结合律,并且对于任意的对象,总存在一个单位态射,使得对于任意的,有
如果对象的类是一个集合,那么这种范畴就被称为小范畴
范畴的例子
以下是一些范畴的例子,读者可以找一两个熟知的例子加深理解。最后一个例子是本文的主要研究对象。
-
集合论:Set 是所有集合和它们彼此之间的全函数构成的范畴
-
拓扑学:Top 是所有拓扑空间和其间的连续函数构成的范畴
-
群论:Grp 是所有群和其间的群同态构成的范畴
-
图论:任何有向图对应于一个小范畴:其对象是图的顶点,其态射是图的路径,其复合态射是路径的连接。称此范畴为有向图的“自由范畴”
-
微分流形:流形和其间的光滑映射构成一个范畴
-
Haskell:Hask是所有类型和其间的函数构成的范畴(把类型看作集合,Hask范畴可以近似为Set范畴)
class Category k where
id :: k a a
-- ^ Identity
(.) :: k b c -> k a b -> k a c
-- ^ Composition
函子(Functor)
只要符合范畴的定义,对象和态射完全可以任意发挥。那么范畴本身是否可以看作一个更高层的范畴的对象呢?
当然可以,范畴的范畴就是:Cat范畴
若将范畴看成是一个更高层的范畴的对象,则两个范畴之间的态射就称为函子(Functor),一个从范畴到范畴的(协变)函子可以定义为:
不难推出以下性质成立:
此外还有反变函子,和协变函子唯一不同的地方在于,它将变换为。自函子(Endofunctor)则是范畴到自身的函子。自函子在Haskell中扮演非常重要的角色,它们相当于类型构造子,因为它可以将类型映射为类型。
在Haskell中,函子的类型类只包括一个fmap。它还需要满足函子律(同上,编译器不会强制检查程序员实现的Functor实例是否满足函子律,需要程序员自己保证。)
class Functor f where
fmap :: (a -> b) -> f a -> f b
-- Functor laws:
fmap id = id
fmap (f . g) = fmap f . fmap g
-- Infix operator:
f <$> x = fmap f x
函子的例子:List
Haskell的数据结构[a]就是Functor类型类的一个实例,fmap就是函子。
instance Functor [a] where
fmap f [] = []
fmap f (x:xs) = f x : fmap xs
-- or --
fmap = map
下面证明它满足函子定律:
-- Identity
fmap id (x:xs) = (id x) : fmap xs = x : fmap xs
-- Composition
(fmap g) . (fmap h) (x : xs)
= fmap g (fmap h (x : xs))
= fmap g ((h x) : fmap h xs)
= (g . h x) : fmap g (fmap h xs)
应用式函子(Applicative)
应用式函子是介于函子和单子之间的结构,它比函子多了一些更有用的函数。
class Functor f => Applicative f where
pure :: a -> f a
(<*>) :: f (a -> b) -> f a -> f b
-- Applicative functor laws:
-- Identity
pure id <*> v = v
-- Composition
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
-- Homomorphism
pure f <*> pure x = pure (f x)
-- Interchange
u <*> pure y = pure ($ y) <*> u
应用式函子的例子
instance Applicative [a] where
pure x = [x]
fs <*> xs = [f x | f <- fs , x <- xs]
-- Test
[(*3), (*2)] <*> [1..4] = [3,6,9,12,2,4,6,8]
-- Proof of Applicative functor laws : left as exercises.
自然变换(Natural transformation)
在范畴论中,一个自然变换是指将一个函子变为另一个函子,使相关范畴的内在结构(即态射间的复合)得以保持,可以将自然变换视作是函子间的态射(这暗示了自然变换是可以合成的)。若是之间的函子,则从到的自然变换是指一族满足下列条件的态射:
-
-
-
利用交换图(Commutative diagram)可以表示为:
如果所有对象的态射都是同构,则称为自然同构(Natural isomorphism),此时函子自然同构于。
在Haskell中也可以定义自然变换,因为自然变换也是一个运算,所以可以定义为一个多态函数:
:set -XRankNTypes
:set -XTypeOperators
type Nat f g = forall x. f x -> g x
对于一个对象和一个函子,将映射到类型,而一个函子将类型映射为,则自然变换的是一个从到的多态函数:
eta :: forall a . F a -> G a
自然变换满足一致性约束,因为函子作用于态射是通过fmap实现的,所以有:
eta_Y . fmap_F f = fmap_G f . eta_X
eta . fmap f = fmap f .eta
读者也注意到了,本文给出了很多恒等式,虽然在实际代码中无法表示,但是可以用于程序推导(编译器也可以利用它们优化)。得益于范畴论的理论支持,函数式编程拥有令人惊讶的表达能力。
自然变换的例子
先看一个简单的数学例子:考虑一个范畴:
设有函子,且有,设是中的恒等函子。设是自然变换,设它在对象处的分量(Components)为:
注意到:
因此是一个自然变换,将映射到了子范畴:
是时候看一下Haskell中的自然变换了。最容易想到的例子就是head函数了,它是Maybe函子和List函子之间的自然变换,功能是返回列表的首个元素,如果是空列表则返回Nothing(不同于Haskell标准库中的head函数)
head ::[a] -> Maybe a
head [] = Nothing
head (x:xs) = x
现在验证它的一致性:
-- for empty list
head (fmap f []) = head [] = Nothing
fmap f (head []) = fmap f Nothing = Nothing
-- for non-empty list
head (fmap f (x:xs)) = head (f x : fmap f xs) = Just (f x)
fmap f (head (x:xs)) = fmap f (Just x) = Just (f x)
自然变换的复合
自然变换也是一种态射,那么它应该能够复合。观察自然变换的交换图,我们发现它与普通的态射不同:它可以有两个结合方向,水平复合和垂直复合。
-
水平复合:设有函子之间的自然变换和函子之间的自然变换,存在一个水平复合(Horizontal composition)。水平复合是函子的组合,显然满足结合律,且存在一个恒等自然变换。
-
垂直复合:设有自然变换,可以得到复合 ,其分量定义为:,此类复合称为垂直复合(Vertical composition),因为自然变换垂直复合就是态射的复合,所以它是可结合的,且存在一个恒等自然变换(Identity natural transformation)使得,利用交换图可以表示为:
复合之后就得到了:
-
Whiskering(我没找到该数学术语的准确翻译,暂且称之为“伸长”运算)是函子和自然变换之间的一个二元运算。设有自然变换和函子,定义自然变换和: 这个运算对于单子的定义非常重要!
函子范畴(Functor category)
上文提到了,函子之间的态射是自然变换。自然变换的水平复合满足结合律,且单位态射就是函子上的恒等自然同构,满足范畴的所有条件,所以我们就得到了一个函子范畴:范畴到范畴之间的所有函子组成的函子范畴,记为。在Haskell中可以定义如下:
-- An alternative definition of natural transformation
newtype Nat f g = Nat {nat :: forall a. f a -> g a }
-- Functor category
instance FunctorCategory Nat where
id = Nat id
Nat f . Nat g = Nat (f . g)
如果以范畴上的自函子为对象,就构成了自函子范畴。
单子(Monad)
如果你在Haskell社区询问别人单子是什么,多半会得到一个回复:单子是自函子范畴上的幺半群。
这个概括是正确的,也是十分抽象的,如果没有一些范畴论知识是无法理解的,好在现在的你已经具备理解它的知识了:)
先看看单子是如何定义的:
在范畴上的单子定义为一个三元组,包含一个自函子和满足特定连贯条件(Coherence condition)的两个自然变换(以下省略水平复合的符号,垂直复合的符号记为):
-
代表自函子
-
是自然变换,是中的单位函子
-
是自然变换
-
单子满足以下两条单子律:
-
,是单位同构。 -
Haskell 中的单子
Haskell中的Monad是Applicative的子类,定义包括>>=运算和return(pure)分别对应了和。当然别忘了还有单子定律:
class Applicative m => Monad m where
-- mu : T (T a) -> T a
(>>=) :: m a -> (a -> m b) -> m b
(>>) :: m a -> m b
-- eta : 1 -> T => r : a -> T a
return :: a -> m a
-- Monad laws:
return a >>= k = k a
-- Left identity ^
m >>= return = m
-- Right identity ^
m >>= (x -> k x >>= h) = (m >>= k) >>= h
-- Associativity ^
-
m是类型构造子,可以构造一个类型m a -
return是类型转换子,可将一个对象嵌入到单子中 -
组合子,表示为中缀算子(>>=),包装一个单体变量,接着把它插入到一个单体函数/表达式之中,结果为一个新的单体值 -
单子律可以解释为单位元和结合律
积范畴(Product Categories)
设有范畴,积范畴是一个积范畴,对象为,且,态射是,。态射的组合即各分量的组合,单位态射是。
幺半群范畴(Monoidal Category)
一个幺半群范畴(张量范畴)是一个带有如下“组件”的范畴
-
一个单位对象 -
一个二元函子(Bifunctor),也就是张量积(Tensor product): -
三组满足以下条件的自然同构映射 -
结合子(Associator): -
单位子(Unitor):左单位子和右单位子
下面证明以上定义的幺半群范畴是一个幺半群。
设是一个幺半群范畴,任取和两个态射,其中是单位对象,注意到它们满足交换律和单位律:
回忆幺半群的定义,不难发现确实是一个幺半群,单位元是
单子的本质
考虑自函子范畴,为使他称为一个幺半群,必须先定义一个张量积:,也就是函子的复合运算。在复合运算下,无需单位子限制,因为就是单位元。注意到函子的复合运算也是可结合的,那么结合子也不需要了。因此自函子范畴是一个幺半群范畴,复合运算就是张量积。
任取自函子和自然变换和,在自函子范畴中,等同于我们选择了和,注意到这些类型签名与单子是一致的。因为复合运算是可结合的,所以满足单子结合律,又注意到,画出交换图不难发现单位律也成立(读者自证不难)。
综上,我们得到了结论:单子是自函子范畴上的幺半群。
总结
受篇幅限制,本文就到此为止了。关于单子其实还有很多有趣的内容没有涉及:Kleisli范畴,单子变换和张量范畴等。本文所涉及的范畴论知识也不过是冰山一角,范畴论的魅力远不止如此。本文的很多数学定义和论证都参考了文末列出的资料,对于意犹未尽的读者,参考文献能够满足你们的好奇心:)
参考资料
Wikipedia nlab Mathematics Stack Exchange Monads in Haskell and Category Theory by Samuel Grahn Monads for functional programming by Philip Wadler Category Theory for Programmers by Bartosz Milewski Monoids: Theme and Variations (Functional Pearl) by Brent A. Yorgey Categories for the Working Mathematician by Mac Lane Notions of computation and monads by Eugenio Moggi
- END -
发表评论