Haskell和自然之代数篇

在上一篇文章 parker liu：Haskell和自然数之基础篇中，我们定义了什么是自然数，给出了自然数的几种定义形式。在这篇文章中，我们继续来探讨自然数，看看自然数的代数结构，自然数和递归、幺半群、F-代数、自由幺半群的关系。

我们再来看一下自然数的定义：

data N = O

| S N -- 使用了递归定义

deriving (Show)

我们可以看到，在这个定义里使用了递归的方式来定义自然数，其中S N是递归步，O是递归的终止。自然数具有一个递归形式，递归层数就是该自然数的大小。于是我们就有了自然数类型N 的形式定义。

我们可以写这么一个函数来将上面定义的自然数N 转换为我们常见的正整数。

nToInt :: N -＞ Int

nToInt O = 0

nToInt (S n) = 1 + nToInt n

--- 在ghci中的运行结果如下

＞ nToInt (S (S (S O))

3

也可以写这么一个函数，将上面定义的自然数N 转换为字母a 组成的字符串。

nToCharAs :: N -＞ [Char]

nToCharAs O = []

nToCharAs (S n) = 'A' : nToCharAs n

--- 在ghci中的运行结果如下

＞ nToCharAs (S (S (S O))

"AAA"

可以看到这两个函数的实现非常的相似，有着同样的结构。如果我们对自然数的定义稍作修改，将自然数N 的构造子S 变换为Cons ()，上面的函数的实现就有着更直观的对应。我们来看修改后的自然数定义：

data NList = NNil

| NCons () NList -- 使用了递归定义

deriving (Show)

我们可以看到，NList 实际上就是类型为()的列表。我们用这个新的自然数定义重新实现上面两个转换函数，于是有：

nlToInt :: NList -＞ Int

nlToInt NNil = 0

--^ NNil

nlToInt (NCons () nl) = 1 + (nlToInt nl)

--^ () NCons NList

--- 在ghci中的运行结果如下

＞ nlToInt (NCons () (NCons () (NCons () NNil))

3

nlToCharAs :: NList -＞ [Char]

nlToCharAs NNil = []

--^ NNil

nlToCharAs (NCons () nl) = 'A' : (nlToCharAs nl)

--^ () NCons NList

--- 在ghci中的运行结果如下

＞ nlToCharAs (NCons () (NCons () (NCons () NNil))

"AAA"

在上面的两个新的转换函数中，NNil 和NCons、() ，以及递归的NList有了直接的一一对应。

在函数nlToInt中，NNil 对应了整数0，NCons对应了整数的加法运算+ ，() 对应了整数1，递归的NList部分则对应了函数nlToInt的递归调用nlToInt nl。

在函数nlToCharAs中，NNil 对应了空列表[]，NCons对应了加法运算+ ，() 对应了字母'A'，递归的NList部分则对应了函数nlToCharAs的递归调用nlToCharAs nl。

我们现在有了更清晰的自然数类型的定义NList，但是这个定义还是使用了递归的形式，在代数数据类型中不好表示和分析这个递归形式。我们接下来使用一些数学技巧来消除这个递归形式。

在上面的自然数类型NList的定义中，可以将NList看成一个非递归函数的不动点，即NList = NListF NList，可以看到，这个非递归的NListF 函数（这是一个类型上的函数）有一个参数，命名为x。当x 是类型NList时，这个函数的结果仍然是NList，于是用x 代替NList，则参考NList的定义我们可以得到这个非递归函数NListF 的定义：

data NListF x = NNilF

| NConsF () x -- 用x 代替了递归定义的NList

那如何从非递归函数NListF 得到其不动点类型NList 呢，我们定义一个如下的不动点函数Fix，其将计算得到任意一个存在不动点的非递归函数F 的不动点Fix F。

-- newtype 表示Fix f 和 f (Fix f) 是等价的，实际上在运行时里面是完全一样的。

newtype Fix f = Fix { unFix :: f (Fix f) } -- Fix f 是函数f 的不动点

-- Fix 和unFix 是一对同构函数

上面的Fix 的定义中，newtype 是Haskell 中的一种特殊的定义新数据类型的方式，表示newtype 定义的新数据类型Fix f 和原来的数据类型f (Fix f) 是等价的，在Haskell 的运行时里的表示是完全一样的，只是在Haskell 中的类型层面上是不同的表示。这样Fix 和unFix 就是一对同构函数，在类型f (Fix f) 和 Fix f 之间转换。为了清晰起见，区别类型上的函数Fix，我们后面用In 来代替Fix，用out 来代替unFix。

newtype Fix f = In { out :: f (Fix f) } -- Fix f 是函数f 的不动点

-- In 和 out 是一对同构函数

有了不动点函数Fix 的定义，我们就可以从非递归函数NListF 得到自然数类型NList 了。具体如下所示：

type NList = Fix NListF -- NList 是NListF 的不动点

到此为止，我们得到了自然数的代数数据类型形式NListF。在代数数据类型的分析中，一般将定义的每个分支作为一个项，不同的分支的组合看成是项的加法。在NListF 的定义中，有两个项，分别是NNilF 和 NConsF () x，这两个项相加就是完整的NListF 的完整定义。另外，Haskell 中的所有类型可以看成是Hask 范畴，这是一个笛卡尔闭范畴（CCC 范畴）。于是，我们可以把NNilF用1 表示，NConsF 表示为乘法，类型() 是x 的一个常数系数，于是NListF 可以看成如下形式的代数数据类型。

Fx＝1＋() × x

这是一个一次多项式，一次项的系数是类型()。在Hask 范畴中，多项式函数是存在不动点的。这个F 函数（NListF 函数）的不动点就是自然数NList，因F 是类型上的函数，定义域是Hask 范畴，值域也是Hask 范畴，所以这是一个Hask 范畴上的自函子。所以也是自函子F （自函子NListF）。

自函子F 的类型变量x 除了可以取值为自函子F 的不动点，即自然数NList，还可以取为Hask 范畴上的其他值。当类型变量x 取值为不动点，即自然数NList 时，由不动点函数的定义，我们有In 函数来将类型F (Fix F) 的值变换为类型Fix F 的值，其有如下的类型签名：

newtype Fix f = In { out :: f (Fix f) }

In :: f (Fix f) -＞ Fix f

type NList = Fix NListF -- NList 是NListF 的不动点

In :: NListF NList -＞ NList

In NNilF = NNil

In (NConsF () n) = NCons () n

当类型变量x 取值不是自函子F 的不动点时，我们同样有一个函数将类型F x 的值变换为x 的值，定义如下：

alg :: f x -＞ x

alg :: NListF x -＞ x

当类型变量x 分别取值Int 和String 时，函数alg 分别有如下的实现：

algInt :: NListF Int -＞ Int

algInt NNilF = 0

algInt (NConsF () i) = 1 + i

algAs :: NListF String -＞ String

algAs NNilF = []

algAs (NConsF () as) = 'A' : as

现在可以看到，自函子F 的类型变量x 每取一个值对应了一个alg 函数，将这两者拼在一起就有(x, alg)。我们可以将(x, alg) 看成一个对象，而类型变量x 和y 之间的函数g :: x -＞ y 和各自的alg 函数满足如下的关系：

g . alg_x = alg_y . F g

nlToInt . In = algInt . NListF nlToInt

nlToCharAs . In = algAs . NListF nlToCharAs

因此，g 可以看成对象(x, alg_x) 和对象(y, alg_y) 之间的态射，x 和y 称为承载对象，所有的(x, alg) 对象和这些对象之间的态射构成了一个范畴，我们称之为F-Alg 范畴。这个范畴的初始对象是(NList, In)，对任意一个承载对象x，都存在一个唯一的态射f: (NList, In) -＞ (x, alg)。

FNList Ff Fx

ln αlg

NList f x

F-Alg范畴初始对象和态射

Fx Fg Fy

αlg-x αlg-y

x g y

F-Alg范畴对象之间的态射

F-Alg 范畴中初始对象到其他对象到态射可以由其他对象的alg 函数得到，将其他对象的alg 函数变换为初始对象到该对象的态射的变换函数称为cata 函数，其定义如下：

type Alg f a = f a -＞ a

cata :: Functor f =＞ Alg f a -＞ Fix f -＞ a

cata alg = go alg

where go alg = alg . fmap (go alg) . out

我们在前一篇文章中定义了自然数N 的加法，同样的NList 也存在加法，定义如下：

plus :: NList -＞ NList -＞ NList

plus NNil nl2 = nl2

plus (NCons () nl) nl2 = NCons () (plus nl nl2)

通过这个加法定义，可以容易的证明其满足如下的单位元定律和结合律。

plus NNil nl == nl plus nl NNil == nl -- 左右单位元定律

plus nl1 (plus nl2 nl3) == plus (plus nl1 nl2) nl3 -- 结合律

因此，自然数类型NList是一个幺半群（monoid），单位元是NNil，二元运算是plus。实际上，对于自函子Fx＝1＋() × x ，我们可以证明这个自函子的F-Alg 范畴中的承载对象x 是一个幺半群。而(NList, In) 是这个范畴的初始对象，因此存在一个唯一的态射f: (NList, In) -＞ (x, alg)，也即f: NList -＞ x，其中f = cata alg，所以NList 是所有承载对象x 构成的幺半群范畴的初始对象，我们称这个初始对象NList 为自由幺半群。

我们适当扩展一下，把自函子Fx＝1＋() × x 中固定的() 作为一个参数a，于是我们就得到如下的自函子：

G α x＝1＋α × x

Haskell形式的定义为：

data ListF a x = NilF

| Cons a x

这也是一个一次多项式，一次项的系数是类型参数a，因此这个自函子G a，即自函子ListF a，也存在一个不动点，我们称之为List a，其定义如下：

data List a = Nil

| Cons a (List a)

令Ga = G a，有自函子Gα＝1＋α × x，我们也同样得到了Ga-Alg 范畴，同理可得，x 也是一个幺半群，自函子Ga 的不动点List a 也是一个自由幺半群。List a就是类型a 的列表，是Haskell中常见的列表类型[a]。

我们再次扩展一下，把自函子G a 中的参数a 扩展为一个函子，乘法× 扩展为函子的张量积运算⨂，而x 则扩展为函子g，1 则是Id 函子。这样有了一个高阶自函子HF f g 的定义：

Hғ f g＝1＋f ⨂ g

这同样是一个一次多项式，一次项的系数是函子参数f ，因此这个自函子HF f，也存在一个不动点。当张量积运算是函子的组合，即(f⨂g)α＝f(g α) 时，自函子HF f 的定义是：

data FreeMF f g a = PureMF a

| FreeMF (f (g a))

其不动点也是一个函子，我们称之为自由单子(Free Monad)，其定义如下：

data Free f a = Pure a

| Free (f (Free f a)

我们也同样得到了HF-Alg 范畴，同理可得，自函子g 也是一个幺半群，高阶自函子HF 的不动点Free f a 也是一个自由幺半群。Free f a就是函子f 组合的列表，是Haskell 中的自由单子。

总结：

在这篇文章中，我们从自然数的递归定义开始，得到了自然数的代数构造，并进一步得到了自然数之上的F-Alg 范畴。在这个F-Alg 范畴中我们知道了自然数是一个幺半群，并且是一个自由幺半群。然后由此扩展得到List a也是一个幺半群，也同时是自由幺半群。最后，我们把F-Alg 扩展为一个高阶自函子的HF-Alg 范畴，并从中得到了自函子上的幺半群，即单子，同时得到了自函子上的自由幺半群，也即自由单子。我们从自然数开始最终得到了自由单子。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。