协慌网

登录 贡献 社区

一个 monad 只是 endofunctors 类别中的一个 monoid,这是什么问题?

谁先说以下?

一个 monad 只是 endofunctors 类别中的一个 monoid,这是什么问题?

在一个不太重要的注解上,这是真的吗?如果可以的话,您能否给出一个解释(希望是一个没有太多 Haskell 经验的人可以理解的解释)?

答案

詹姆斯 · 艾里(James Iry)的这种特别措辞来自他极富娱乐性的《 简明,不完整和大部分错误的编程语言历史》 ,他在小说中将其归因于菲利普 · 沃德勒(Philip Wadler)。

原始报价摘自 Saunders Mac Lane的《工作数学家的类别》,这是类别理论的基础文章之一。 在上下文中,这可能是确切了解其含义的最佳位置。

但是,我会刺。原来的句子是这样的:

总而言之,X 中的单子仅是 X 的终结者类别中的一个单义词,乘积 × 被终结者的组成所取代,单位由终结者的身份设定。

X这里是一个类别。 Endofunctors 是从一个类别到其自身的Functor (就函数式程序员而言,通常是 Functor 的所有函子,因为它们主要只处理一个类别;类型的类别 - 但我离题了)。但是您可以想象另一个类别,即 “ X 上的endofunctors” 类别。这是一类,其中的对象是内泛函子,而态射是自然变换。

在这些终结者中,有些可能是单子。哪一个是单子?确切地说,在特定意义上是单调的。与其说出从单子到 Monoid 的确切映射(因为 Mac Lane 的性能远远超出我的期望),不如将它们各自的定义放在一起,让您进行比较:

一个半身像是...

  • 一套S
  • 一个运算, •:S×S→S
  • S的元素, e:1→S

... 满足以下法律:

  • (a•b)•c = a•(b•c) ,对于S 中的所有 abc
  • e•a = a•e = a ,对于S 中的所有 a

一个单子是...

  • endofunctor T:X→X (在 Haskell 中,类型* -> *的类型构造函数,带有Functor实例)
  • 自然变换μ:T×T→T ,其中×表示函子组成( μ在 Haskell 中称为join
  • 自然变换η:I→T ,其中I是 X上的恒等符( η在 Haskell 中称为return

... 满足以下法律:

  • μ∘Tμ=μ∘μT
  • μ∘Tη=μηT= 1 (恒等式自然转化)

稍作斜视,您也许就能看到这两个定义都是同一抽象概念的实例。

首先,我们将要使用的扩展和库:

{-# LANGUAGE RankNTypes, TypeOperators #-}

import Control.Monad (join)

其中, RankNTypes是唯一对以下内容绝对必要的一种。 我曾经写过对RankNTypes的解释,有些人似乎发现它很有用,因此我将参考它。

引用汤姆 · 克罗基特的出色答案,我们有:

一个单子是...

  • 一个 endofunctor, T:X-> X
  • 自然变换, μ:T×T-> T ,其中×表示函子组成
  • 自然变换η:I-> T ,其中I是 X上的恒等 endofunctor

... 满足以下法律:

  • μ(μ(T×T)×T))=μ(T×μ(T×T))
  • μ(η(T))= T =μ(T(η))

我们如何将其转换为 Haskell 代码?好吧,让我们从自然转换的概念开始:

-- | A natural transformations between two 'Functor' instances.  Law:
--
-- > fmap f . eta g == eta g . fmap f
--
-- Neat fact: the type system actually guarantees this law.
--
newtype f :-> g =
    Natural { eta :: forall x. f x -> g x }

A 型的形式的f :-> g类似于一个功能类型,但它的思想为两种类型(种之间的函数来代替* ),把它作为两个函子(各种之间的态射* -> * )。例子:

listToMaybe :: [] :-> Maybe
listToMaybe = Natural go
    where go [] = Nothing
          go (x:_) = Just x

maybeToList :: Maybe :-> []
maybeToList = Natural go
    where go Nothing = []
          go (Just x) = [x]

reverse' :: [] :-> []
reverse' = Natural reverse

基本上,在 Haskell 中,自然转换是从某种类型的fx到另一种类型的gxx ,使得调用者 “无法访问” x 类型变量。因此,例如, sort :: Ord a => [a] -> [a]不能转换为自然转换,因为它对我们可以实例化a类型是 “挑剔的”。我经常想到的一种直观方法是:

  • 函子是一种在不触及结构的情况下操作某物内容的方法。
  • 自然转换是一种无需触摸或查看内容即可对事物的结构进行操作的方法。

现在,让我们解决这个定义的子句。

第一个子句是 “ endofunctor, T:X-> X” 。嗯, Functor都是人们所说的 “Hask 类别” 的终结者,其对象是 Haskell 类型( *的类型),其态射是 Haskell 函数。这听起来像是一个复杂的声明,但实际上是一个非常琐碎的声明。这意味着Functor f :: * -> *为您提供了为任何a :: *和函数fmap f :: fa -> fb在任何f :: a -> b fa :: * f :: a -> b ,并且它们遵守函子定律。

第二条: Identity仿函数(随平台提供,因此您只需导入即可)是通过以下方式定义的:

newtype Identity a = Identity { runIdentity :: a }

instance Functor Identity where
    fmap f (Identity a) = Identity (f a)

Monad实例t以这种方式编写来自 Tom Crockett 定义的自然变换η:I-> T

return' :: Monad t => Identity :-> t
return' = Natural (return . runIdentity)

第三条:Haskell 中两个函子的组成可以通过这种方式定义(这也随平台一起提供):

newtype Compose f g a = Compose { getCompose :: f (g a) }

-- | The composition of two 'Functor's is also a 'Functor'.
instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose fga) = Compose (fmap (fmap f) fga)

因此,汤姆 · 克罗基特(Tom Crockett)定义中的自然变换μ:T×T-> T 可以这样写:

join' :: Monad t => Compose t t :-> t
join' = Natural (join . getCompose)

声明这是 endofunctors 类别中的一个 monoid,则表示Compose (部分应用于其前两个参数)是关联的, Identity是其标识元素。即,以下同构成立:

  • Compose f (Compose gh) ~= Compose (Compose fg) h
  • Compose f Identity ~= f
  • Compose Identity g ~= g

这些都很容易证明,因为ComposeIdentity都定义为newtype ,并且 Haskell Reports 将newtype newtype的数据构造函数的参数类型之间的同构。因此,例如,让我们证明Compose f Identity ~= f

Compose f Identity a
    ~= f (Identity a)                 -- newtype Compose f g a = Compose (f (g a))
    ~= f a                            -- newtype Identity a = Identity a
Q.E.D.

这里的答案在定义 monoid 和 monad 方面做得非常出色,但是,它们似乎仍然无法回答这个问题:

在一个不太重要的注解上,这是真的吗?如果可以的话,您能否给出一个解释(希望是一个没有太多 Haskell 经验的人可以理解的解释)?

这里遗漏的问题的症结在于 “monoid” 的不同概念,更确切地说是所谓的分类- 在 monoidal 类别中的 monoid。可悲的是,Mac Lane 的书本身使人非常困惑

总而言之,在一个单子X是正好在 endofunctors 的类别幺半群X ,具有产品×由 endofunctors 的组合物和单位组替换由身份 endofunctor。

主要困惑

为什么这令人困惑? X “endofunctors 类别中的 monoid”。取而代之的是,这句话建议将所有 endofunctors集合内的一个类群与函子组成一起作为二元运算,将身份函子作为一个类群单元。它工作得非常好,并且可以将包含身份函子并在函子组成下封闭的 endofunctors 的任何子集变成一个 monoid。

但这并不是正确的解释,这本书在那个阶段还没有弄清楚。 Monad f固定的终结子函数,而不是在合成条件下封闭的终结子函数子集。一种常见的结构是使用f通过取该组所有的以产生独异k倍组合物f^k = f(f(...))f与本身,包括k=0对应于身份f^0 = idk>=0的所有这些幂的集合S确实是一个 mono 半同形体,“乘积 × 被终结者的组成所取代,单位由身份终结者所设定”。

但是:

  • 可以为任何函子f S ,甚至可以为X它是由f
  • 由函子组成和恒等函子给出S的单曲面结构f是否为单核无关。

为了使事情更加混乱,您可以从目录中看到 “单曲面类别中的 Monoid” 的定义。但是,理解这一概念对于理解与 monad 的联系绝对至关重要。

(严格)单等分类

转到有关 Monoids 的第七章(比 Monads 的第六章晚),我们发现所谓的严格 Monoidal 类别的定义为 Triple (B, *, e) ,其中B是类别*: B x B-> Bbifunctor (固定了其他组件的每个组件的 functor), e B的单位对象,满足关联性和单位定律:

(a * b) * c = a * (b * c)
a * e = e * a = a

对于任何对象a,b,cB ,以及对于任何态射相同的身份a,b,ce取代id_e ,身份态射e 。现在具有启发性的观察结果是,在我们感兴趣的情况下,其中B X的端尾类的范畴,具有自然转化为同态, *函子的组成和e身份函子都满足所有这些定律,可以直接验证。

这本书中的定义是 “松弛”单项类的定义,其中法律仅对满足所谓相干关系的某些固定自然变换进行模运算,但是这对于我们的终结论者类而言并不重要。

id 面体类别中的面体

最后,在第七章的第 3 节 “Monoids” 中,给出了实际的定义:

(B, *, e)中的一个单曲面c是具有两个箭头(同晶) B的对象

mu: c * c -> c
nu: e -> c

使 3 个图可交换。回想一下,在我们的案例中,这些是 endofunctors 类别中的态射,它们是自然转换,对应于 monad 的joinreturn *更明确,用c^2 c * c时,连接变得更加清晰,其中c是我们的单子。

最后,请注意,为一般(非严格)单曲面类别编写了 3 个交换图(按单曲面类别中的单曲面定义),而在我们的情况下,作为单曲面类别的一部分出现的所有自然变换实际上都是恒等式。这将使这些图与 monad 定义中的图完全相同,从而使对应关系完整。

结论

总而言之,根据定义,任何 monad 都是 endofunctor,因此是 endofunctors 类别中的一个对象,其中 monadic joinreturn运算符满足该特定(严格)monoidal 类别中的 monoid 的定义。反之亦然,根据定义,endofunctors 的单曲面类中的任何一个单面体都是由(c, mu, nu) ,例如,在我们的情况下是自然变换,满足与 monad 相同的定律。

最后,请注意(经典)monoid 和更简单的 monoidal 类别中的 monoid 之间的主要区别。上面的两个箭头munu不再是二进制运算和集合中的一个单元。相反,您有一个固定的 endofunctor c 。尽管书中有令人困惑的注释,但函子组成*和身份函子本身并不能提供 monad 所需的完整结构。

另一种方法是与A的所有自映射C进行比较,其中二元运算是合成,可以看到将标准笛卡尔积C x C映射到C 。传递到分类的 monoid,我们用函子组成* x ,并且二元运算被替换为从c * cc mu ,这是join运算符的集合

join: c(c(T))->c(T)

对于每个对象T (编程类型)。可以用固定的单点集的地图图像标识的经典类四面体中的标识元素,用return运算符的集合替换

return: T->c(T)

但是现在不再有笛卡尔积,所以没有成对的元素,也就没有二进制运算。