跳至内容

Haskell/范畴论

来自 Wikibooks,开放世界中的开放书籍

本文试图概述范畴论,因为它适用于 Haskell。为此,将在数学定义旁边给出 Haskell 代码。不会完全遵循严格性,相反,我们希望让读者直观地了解范畴论的概念以及它们如何与 Haskell 相关联。

范畴简介

[编辑 | 编辑源代码]
一个简单的范畴,有三个对象 ABC,三个恒等态射 ,以及另外两个态射 。第三个元素(态射如何组合的规范)没有显示。

本质上,范畴是一个简单的集合。它有三个组成部分

  • 对象 的集合。
  • 态射 的集合,每个态射将两个对象(源对象目标对象)联系在一起。(这些有时被称为 箭头,但我们在这里避免使用该术语,因为它在 Haskell 中有其他含义。)如果 f 是一个源对象为 C,目标对象为 B 的态射,我们写成 .
  • 组合 这些态射的概念。如果 是两个态射,它们可以被组合,得到一个态射 .

很多东西都构成范畴。例如,Set 是所有集合的范畴,其中态射是标准函数,组合是标准函数组合。(范畴名称通常以粗体表示。)Grp 是所有群的范畴,其中态射是保留群运算的函数(群同态),即对于任意两个群,G 的运算为 *H 的运算为 ·,一个函数 Grp 中的态射,如果

虽然看起来态射总是函数,但情况并非总是如此。例如,任何偏序集 (P, ) 定义了一个范畴,其中对象是 P 的元素,并且在任意两个对象 AB 之间存在态射当且仅当 。此外,允许存在具有相同源对象和目标对象的多个态射;使用 Set 示例, 都是具有源对象 (实数集)和目标对象 的函数,但它们绝对不是同一个态射!

范畴律

[edit | edit source]

范畴需要遵循三个定律。首先,也是最简单的,态射的复合需要是 结合的。用符号表示,

在 Haskell 和大多数数学中,态射是从右到左应用的,因此对于 ,首先应用 g,然后应用 f

其次,范畴需要在复合运算下是 封闭的。因此,如果 ,那么范畴中一定存在某个态射 ,使得 。我们可以使用以下范畴来观察它是如何工作的

fg 都是态射,因此我们必须能够将它们复合并得到范畴中的另一个态射。那么哪个态射是 ?唯一的选择是 。类似地,我们看到

最后,给定一个类别C,对于每个对象,都需要一个恒等态射,它是与其他态射复合的恒等元素。准确地说,对于每个态射

Hask,Haskell 类别

[edit | edit source]

本文将关注的重点是Hask类别,它将 Haskell 类型视为对象,Haskell 函数视为态射,并使用(.)作为复合运算符:对于类型AB的函数f :: A -> BHask中的态射。我们可以轻松验证第一和第二定律:我们知道(.)是一个结合函数,并且显然,对于任何fgf . 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

但是,为了简单起见,当含义明确时,我们将忽略这种区别。

练习
  • 如上所述,任何偏序(P)都是一个类别,其对象是P的元素,元素ab之间的态射当且仅当a b。上面哪条定律保证了的传递性?
  • (较难)如果我们在上面示例中添加另一个态射,如下所示,它将不再是一个类别。为什么?提示:考虑复合运算符的结合性。

函子

[edit | edit source]
两个类别之间的一个函子,。需要注意的是,对象AB都被映射到中的同一个对象,因此g变成具有相同源对象和目标对象(但不一定是恒等元素)的态射, 变成同一个态射。显示对象映射的箭头以虚线、浅橄榄色显示。显示态射映射的箭头以虚线、浅蓝色显示。

因此我们有一些类别,它们具有将对象关联起来的对象和态射。类别理论中的下一个重大主题是函子,它将类别关联起来。函子本质上是类别之间的变换,因此给定类别CD,函子

  • C中的任何对象A映射到D中的
  • C中的态射映射到D中的

函子一个典型的例子是遗忘函子,它将群映射到它们的基础集合,将群同态映射到在集合而不是群上定义的行为相同的函数。另一个例子是幂集函子,它将集合映射到它们的幂集,并将函数映射到函数,它以输入并返回,即Uf下的像,定义为。对于任何范畴C,我们可以定义一个称为C上的恒等函子的函子,或,它只是将对象映射到它们自身,将态射映射到它们自身。这将在后面的单子定律部分中被证明是有用的。

再次强调,函子必须服从一些公理。首先,给定对象A上的恒等态射必须是上的恒等态射,即

其次,函子必须在态射复合上分配,即

练习
对于右边给出的图表,检查这些函子定律。

Hask上的函子

[edit | edit source]

您可能在 Haskell 中见过的 Functor 类型类实际上与函子的范畴论概念相关。请记住,函子有两个部分:它将一个范畴中的对象映射到另一个范畴中的对象,并将第一个范畴中的态射映射到第二个范畴中的态射。Haskell 中的函子是从 Haskfunc 的,其中 funcHask 的一个子范畴,仅定义在该函子的类型上。例如,列表函子是从 HaskLst 的,其中 Lst 是仅包含 列表类型 的范畴,即任何类型 T[T]Lst 中的态射是在列表类型上定义的函数,即对于类型 TU 的函数 [T] -> [U]。这如何与 Haskell 类型类 Functor 联系起来呢?回顾其定义

class Functor (f :: * -> *) where
  fmap :: (a -> b) -> f a -> f b

让我们举一个示例实例,

instance Functor Maybe where
  fmap f (Just x) = Just (f x)
  fmap _ Nothing  = Nothing

关键部分在于:类型构造器 Maybe 将任何类型 T 转换为一个新类型 Maybe T。此外,fmap 限制在 Maybe 类型上,它将函数 a -> b 转换为函数 Maybe a -> Maybe b。但仅此而已!我们定义了两个部分,一个将 Hask 中的对象映射到另一个范畴中的对象(即 Maybe 类型和在 Maybe 类型上定义的函数),另一个将 Hask 中的态射映射到该范畴中的态射。因此,Maybe 是一个函子。

关于 Haskell 函子的一个有用的直觉是它们代表可以映射的类型。这可以是列表或 Maybe,也可以是树等更复杂结构。使用 fmap 可以编写执行某些映射的函数,然后可以将任何函子结构传递到该函数中。例如,您可以编写一个通用的函数,它涵盖所有 Data.List.map、Data.Map.map、Data.Array.IArray.amap 等等。

函子公理呢?多态函数 id 代替了任何 A,因此第一个定律指出

fmap id = id

考虑到我们上面的直觉,这说明对一个结构进行映射,而对每个元素都不做任何操作,等同于不做任何操作。其次,态射复合就是 (.),所以

fmap (f . g) = fmap f . fmap g

这个第二个定律在实践中非常有用。将函子想象成列表或类似的容器,右侧是一个两遍算法:我们对结构进行映射,执行 g,然后再次对其进行映射,执行 f。函子公理保证我们可以将其转换为一个执行 f . g 的单遍算法。这是一个称为 融合 的过程。

练习
检查 Maybe 和列表函子的定律。

将范畴论概念转换为 Haskell

[edit | edit source]

函子提供了一个很好的例子,说明范畴论是如何被转换为 Haskell 的。需要记住的关键点是

  • 我们在 Hask 及其子范畴中工作。
  • 对象是类型。
  • 态射是函数。
  • 接受一个类型并返回另一个类型的函数是类型构造器。
  • 接受一个函数并返回另一个函数的函数是高阶函数。
  • 类型类及其提供的多态性,为捕捉范畴论中事物通常在多个对象上定义这一事实提供了一种很好的方式。

单子

[edit | edit source]
unitjoin,对于给定单子中的每个对象,必须存在的两个态射。

单子显然是 Haskell 中一个极其重要的概念,事实上它们最初来自范畴论。单子 是一种特殊的函子,从一个范畴到同一个范畴,它支持一些额外的结构。因此,让我们从定义开始。单子是一个函子 ,以及对于 C 中的每个对象 X,有两个态射[2]

当所讨论的单子很明显时,我们会省略这些函数的 M 上标,只讨论一些 X

那么,让我们看看这如何转换为 Haskell 类型类 Monad。

class Functor m => Monad m where
  return :: a -> m a
  (>>=)  :: m a -> (a -> m b) -> m b

Functor m 的类约束确保我们已经有了函子结构:对象和态射的映射。return 是任何 X 的(多态)类似物。但是我们遇到了一个问题。尽管 return 的类型看起来与 unit 的类型非常相似;另一个函数 (>>=),通常称为 bind,与 join 没有任何相似之处。然而,另一个单子函数 join :: Monad m => m (m a) -> m a,看起来很相似。事实上,我们可以从彼此中恢复 join(>>=)

join :: Monad m => m (m a) -> m a
join x = x >>= id

(>>=) :: Monad m => m a -> (a -> m b) -> m b
x >>= f = join (fmap f x)

因此,指定一个单子的 `return`、`fmap` 和 `join` 等同于指定它的 `return` 和 `(>>=)`. 事实上,在范畴论中定义单子的正常方式是给出 *unit* 和 *join*,而 Haskell 程序员更喜欢给出 `return` 和 `(>>=)`.[3] 很多时候,范畴论的方式更有意义。只要你拥有某种结构 * 以及将任何对象 * 转化为 的自然方式,以及将 转化为 的方式,你很可能就拥有一个单子。在接下来的示例部分中,我们可以看到这一点。

示例:幂集函子也是一个单子

[edit | edit source]

上面描述的幂集函子 构成了一个单子。对于任何集合 *S*,你都有一个 ,它将元素映射到它们的单元素集合。请注意,这些单元素集合都是 *S* 的平凡子集,因此 返回 *S* 的幂集中的元素,这是必需的。此外,你可以定义一个函数 ,如下所示:我们接收一个输入 。这是

  • *S* 的幂集的幂集的成员。
  • 因此是 *S* 的所有子集的集合的所有子集的集合的成员。
  • 因此是 *S* 的子集的集合

然后我们返回这些子集的并集,得到 *S* 的另一个子集。符号上,

.

因此 *P* 是一个单子[4].

事实上,*P* 几乎等同于列表单子;除了我们谈论的是列表而不是集合,它们几乎是一样的。请比较



Set 上的幂集函子
函数类型 定义
给定一个集合 *S* 和一个态射
Haskell 中的列表单子
函数类型 定义
给定类型 T 和函数 f :: A -> B
fmap f :: [A] -> [B] fmap f xs = [ f a | a <- xs ]
return :: T -> [T] return x = [x]
join :: [[T]] -> [T] join xs = concat xs

单子定律及其重要性

[edit | edit source]

就像函子为了被称为函子必须遵守某些公理一样,单子也有一些自己的公理。我们首先列出它们,然后翻译成 Haskell,最后看看它们为什么如此重要。

给定一个单子 和一个态射 对于 ,

现在,Haskell 翻译应该不言自明了

  1. join . fmap join = join . join
  2. join . fmap return = join . return = id
  3. return . f = fmap f . return
  4. join . fmap (fmap f) = fmap f . join

(记住 fmap 是函子的作用于态射的部分。) 这些定律乍一看有点难以理解。这些定律到底意味着什么,为什么它们应该对单子成立?让我们来探索一下这些定律。

第一定律

[edit | edit source]

join . fmap join = join . join

列表的第一定律的演示。记住 joinconcatfmap 是列表单子中的 map

为了理解这个定律,我们首先以列表为例。第一定律提到了两个函数,join . fmap join(左侧)和 join . join(右侧)。这些函数的类型会是什么?记住 join 的类型是 [[a]] -> [a](我们现在只谈论列表),所以这两个类型的类型都是 [[[a]]] -> [a](它们相同的事实很有用;毕竟,我们试图证明它们完全相同函数!)。所以我们有一个列表的列表的列表。然后,左侧对这个三层列表执行 fmap join,然后对结果使用 joinfmap 只是列表中熟悉的 map,所以我们首先对顶层列表中每个列表的列表进行映射,将它们连接成一个列表。因此,之后我们有一个列表的列表,然后我们将其运行到 join 中。总而言之,我们“进入”顶层,将第二层和第三层折叠起来,然后将这个新层与顶层折叠起来。

右侧呢?我们首先对我们的列表的列表的列表运行 join。尽管这是三层,而你通常将一个两层列表应用于 join,但这仍然会起作用,因为 [[[a]]] 只是 [[b]],其中 b = [a],所以从某种意义上说,一个三层列表只是一个两层列表,但最后一层不是“扁平”的,而是由另一个列表组成。因此,如果我们将我们的列表的列表(的列表)应用于 join,它将把最外层的两层扁平化成一层。由于第二层不是扁平的,而是包含第三层,因此我们最终仍然会得到一个列表的列表,另一个 join 会将其扁平化。总结一下,左侧将把内层的两层扁平化成一个新层,然后将这个层与最外层扁平化。右侧将首先扁平化外层的两层,然后将这个层与最内层扁平化。这两个操作应该是等效的。这有点像 join 的结合律。

Maybe 也是一个单子,有

return :: a -> Maybe a
return x = Just x

join :: Maybe (Maybe a) -> Maybe a
join Nothing         = Nothing
join (Just Nothing)  = Nothing
join (Just (Just x)) = Just x

因此,如果我们有一个层的 Maybe(即,它可能是 NothingJust NothingJust (Just Nothing) 或者 Just (Just (Just x))),第一定律表示先折叠内层的两层,然后与外层折叠完全等效于先折叠外层,然后与最内层折叠。

练习
使用一些示例验证列表和 Maybe 单子是否确实遵循此定律,以准确了解层级扁平化的工作原理。

第二定律

[编辑 | 编辑源代码]

join . fmap return = join . return = id

那么第二定律呢?同样,我们将从列表的例子开始。第二定律中提到的两个函数都是 [a] -> [a] 类型的函数。左侧表示一个函数,它遍历列表,将每个元素 x 转换为其单例列表 [x],这样最终我们就剩下一个单例列表的列表。这个两层列表使用 join 再次扁平化为单层列表。然而,右侧则将整个列表 [x, y, z, ...] 转换为列表的单例列表 [[x, y, z, ...]],然后将两层再次扁平化为一层。这条定律不太容易快速说明,但它本质上说的是,将 return 应用于单子值,然后 join 结果,无论是在顶层内部还是外部执行 return,都应该具有相同的效果。

练习
证明 Maybe 单子的这条第二定律。

第三和第四定律

[编辑 | 编辑源代码]

return . f = fmap f . return

join . fmap (fmap f) = fmap f . join

最后两条定律表达了我们对单子的期望行为的更直观的事实。最简单的理解其真伪的方法是将其扩展为使用扩展形式

  1. \x -> return (f x) = \x -> fmap f (return x)
  2. \x -> join (fmap (fmap f) x) = \x -> fmap f (join x)
练习
通过探索它们的含义,以类似于我们解释第一和第二定律的方式,说服自己这些定律应该适用于任何单子。

对 do 块的应用

[编辑 | 编辑源代码]

嗯,我们对单子必须支持的定律有了直观的描述,但这为什么很重要呢?当我们考虑 do 块时,答案就变得显而易见了。回想一下,do 块只是涉及 (>>=) 的语句组合的语法糖,正如通常的翻译所证明的那样

do { x }                 -->  x
do { let { y = v }; x }  -->  let y = v in do { x }
do { v <- y; x }         -->  y >>= \v -> do { x }
do { y; x }              -->  y >>= \_ -> do { x }

还要注意,我们可以使用我们上面定律中的 return(>>=) 来证明通常被引用为单子定律的东西(证明在某些情况下有点繁琐,如果你想跳过它们,请随意跳过)

  1. return x >>= f = f x。证明
       return x >>= f
     = join (fmap f (return x)) -- By the definition of (>>=)
     = join (return (f x))      -- By law 3
     = (join . return) (f x)
     = id (f x)                 -- By law 2
     = f x
    
  2. m >>= return = m。证明
       m >>= return
     = join (fmap return m)    -- By the definition of (>>=)
     = (join . fmap return) m
     = id m                    -- By law 2
     = m
    
  3. (m >>= f) >>= g = m >>= (\x -> f x >>= g)。证明(回想一下 fmap f . fmap g = fmap (f . g)
       (m >>= f) >>= g
     = (join (fmap f m)) >>= g                          -- By the definition of (>>=)
     = join (fmap g (join (fmap f m)))                  -- By the definition of (>>=)
     = (join . fmap g) (join (fmap f m))
     = (join . fmap g . join) (fmap f m)
     = (join . join . fmap (fmap g)) (fmap f m)         -- By law 4
     = (join . join . fmap (fmap g) . fmap f) m
     = (join . join . fmap (fmap g . f)) m              -- By the distributive law of functors
     = (join . join . fmap (\x -> fmap g (f x))) m
     = (join . fmap join . fmap (\x -> fmap g (f x))) m -- By law 1
     = (join . fmap (join . (\x -> fmap g (f x)))) m    -- By the distributive law of functors
     = (join . fmap (\x -> join (fmap g (f x)))) m
     = (join . fmap (\x -> f x >>= g)) m                -- By the definition of (>>=)
     = join (fmap (\x -> f x >>= g) m)
     = m >>= (\x -> f x >>= g)                          -- By the definition of (>>=)
    

这些使用 return(>>=) 的新单子定律可以翻译成 do 块表示法。

无点风格 do 块风格
return x >>= f = f x do { v <- return x; f v } = do { f x }
m >>= return = m do { v <- m; return v } = do { m }
(m >>= f) >>= g = m >>= (\x -> f x >>= g)
   do { y <- do { x <- m; f x };
        g y }
 =
   do { x <- m;
        y <- f x;
        g y }

现在,单子定律就变成了关于 do 块应该如何工作的常识性陈述。如果其中一条定律失效,用户就会感到困惑,因为你将无法像预期的那样在 do 块中进行操作。本质上,单子定律是可用性指南。

练习

事实上,我们给出的两种定律版本

-- Categorical:
join . fmap join = join . join
join . fmap return = join . return = id
return . f = fmap f . return
join . fmap (fmap f) = fmap f . join

-- Functional:
m >>= return = m
return m >>= f = f m
(m >>= f) >>= g = m >>= (\x -> f x >>= g)

完全等价。我们已经证明可以从范畴定律中恢复函数定律。反过来,从函数定律出发,证明范畴定律成立。记住以下定义可能会有所帮助

join m = m >>= id
fmap f m = m >>= return . f
感谢 Yitzchak Gale 提供了这项练习建议。

在本章中,我们已经走得很远。我们已经了解了什么是范畴,以及它们如何应用于 Haskell。我们介绍了范畴论的基本概念,包括函子,以及一些更高级的主题,比如单子,并看到了它们对 Haskell 惯用语法的关键作用。我们没有涵盖一些对我们的目标来说不必要的范畴论基础知识,比如自然变换,而是为 Haskell 结构背后的范畴基础提供了直观的感受。

备注

  1. 实际上,这里有一个细微之处:因为 (.) 是一个惰性函数,如果 fundefined,我们就有 id . f = \_ -> ⊥。现在,虽然这在所有意图和目的上似乎等同于 ,但实际上你可以使用严格化函数 seq 将它们区分开来,这意味着最后一条范畴定律被破坏了。我们可以定义一个新的严格组合函数 f .! g = ((.) $! f) $! g,它使 Hask 成为一个范畴。然而,我们将继续使用正常的 (.),并将任何差异归因于 seq 实际上破坏了很多很好的语言属性这一事实。
  2. 经验丰富的范畴论者会注意到我们在这里简化了一些东西;与其将 单位连接 作为自然变换,不如将它们的自然性作为额外公理(定律 3 和 4)与标准单子定律(定律 1 和 2)一起添加。理由是简单;我们不是要教授整个范畴论,只是为 Haskell 中的一些结构提供范畴背景。你可能还会注意到,我们给这些态射起了类似于它们的 Haskell 类似物的名称,因为名称 并没有提供太多的直觉。
  3. 这可能是由于 Haskell 程序员喜欢将单子视为一种具有共同特征的顺序执行计算的方法,而在范畴论中,各种结构的容器方面更为突出。join 自然地适用于容器(将容器的两个层级压缩为一个),而 (>>=) 是自然的顺序执行操作(执行某项操作,将结果馈送到其他操作中)。
  4. 如果你能证明某些定律成立,我们将在下一节中探讨。
华夏公益教科书