下面是谁先说的?
单子只是内函子类别中的一个幺半群,有什么问题?
在不太重要的一点上,这是真的吗?如果是这样,您能否给出解释(希望没有太多 Haskell 经验的人可以理解)?
下面是谁先说的?
单子只是内函子类别中的一个幺半群,有什么问题?
在不太重要的一点上,这是真的吗?如果是这样,您能否给出解释(希望没有太多 Haskell 经验的人可以理解)?
这个特别的措辞来自 James Iry,来自他非常有趣的Brief, Incomplete and Mostly Wrong History of Programming Languages,其中他虚构地将其归因于 Philip Wadler。
原始引述来自 Saunders Mac Lane 在为工作数学家分类中的文章,这是范畴论的基础文本之一。这是在 context 中,这可能是准确了解其含义的最佳场所。
但是,我会打一针。原句是这样的:
总而言之,X 中的单子只是 X 的内函子类别中的一个幺半群,乘积 × 被内函子的组合替换,单位由恒等函子设置。
X这里是一个类别。Endofunctors 是从一个类别到其自身的函子(就函数式程序员而言,这通常都是s,因为他们主要处理一个类别;类型的类别 - 但我离题了)。 Functor
但是您可以想象另一个类别,即“ X上的内函子”类别。这是一个范畴,其中对象是内函子,态射是自然变换。
在这些内函子中,其中一些可能是单子。哪些是单子?正是那些在特定意义上是幺半群的。与其详细说明从 monad 到 monoid 的确切映射(因为 Mac Lane 做得比我希望的要好得多),我只是将它们各自的定义并排放置并让您比较:
* -> *
带有一个Functor
实例)join
在 Haskell中称为)return
在 Haskell中被称为)稍稍眯起眼睛,您可能会发现这两个定义都是同一个抽象概念的实例。
首先,我们将要使用的扩展和库:
{-# LANGUAGE RankNTypes, TypeOperators #-}
import Control.Monad (join)
其中,RankNTypes
是唯一对以下内容绝对必要的。我曾经写过RankNTypes
一些人似乎觉得有用的解释,所以我会参考一下。
引用Tom Crockett 的出色回答,我们有:
一个单子是...
- 一个内函子,T : X -> X
- 自然变换,μ : T × T -> T,其中×表示函子组合
- 自然变换η : I -> T,其中I是X上的恒等函数
...满足这些法律:
- μ(μ(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 }
形式的类型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 中,自然转换是从某种类型f x
到另一种类型的函数,g x
使得x
调用者“无法访问”类型变量。因此,例如,sort :: Ord a => [a] -> [a]
不能进行自然转换,因为它对于我们可以实例化哪些类型是“挑剔的” a
。我经常用来思考这个问题的一种直观方式是:
现在,解决这个问题,让我们处理定义的子句。
第一个子句是“一个内函子,T : X -> X ”。好吧,Functor
Haskell 中的 every 都是人们所说的“Hask 范畴”中的内函子,其对象是 Haskell 类型(种类*
),其态射是 Haskell 函数。这听起来像是一个复杂的陈述,但它实际上是一个非常微不足道的陈述。这意味着 aFunctor f :: * -> *
为您提供了f a :: *
为 any构造类型和从any 中构造a :: *
函数的方法,并且这些遵循函子定律。fmap f :: f a -> f b
f :: a -> b
第二个子句:Identity
Haskell 中的函子(平台自带,所以你可以直接导入)是这样定义的:
newtype Identity a = Identity { runIdentity :: a }
instance Functor Identity where
fmap f (Identity a) = Identity (f a)
因此,Tom Crockett 定义的自然变换η : I -> TMonad
对于任何实例都可以这样写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)
这是内函子类别中的幺半群的陈述意味着Compose
(部分应用于仅其前两个参数)是关联的,这Identity
就是它的单位元素。即,以下同构成立:
Compose f (Compose g h) ~= Compose (Compose f g) h
Compose f Identity ~= f
Compose Identity g ~= g
这些很容易证明,因为Compose
和Identity
都定义为newtype
,并且 Haskell 报告将 的语义定义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.
这里的答案在定义幺半群和单子方面做得很好,但是,他们似乎仍然没有回答这个问题:
在不太重要的一点上,这是真的吗?如果是这样,您能否给出解释(希望没有太多 Haskell 经验的人可以理解)?
这里缺少的问题的症结在于“monoid”的不同概念,更准确地说是所谓的分类——monoid 类别中的monoid。可悲的是,Mac Lane 的书本身就让人很困惑:
总而言之,单子 in
X
只是 的 endofunctors 类别中的一个幺半群X
,乘积×
由 endofunctors 的组合替换,单位由恒等 endofunctor 设置。
为什么这令人困惑?因为它没有定义什么是“内函子范畴中的幺半群” X
。相反,这句话建议在所有内函子集合中取一个幺半群,将函子组合作为二元运算,将恒等函子作为一个幺半群单元。它工作得非常好,并变成一个包含恒等函子并在函子组合下封闭的内函子的任何子集的幺半群。
然而,这不是正确的解释,这本书在那个阶段未能阐明。Monadf
是一个固定的内函子,而不是在合成下封闭的内函子的子集。一种常见的构造是通过使用其自身的所有折叠组合的集合f
来生成一个幺半群,包括对应于恒等式的组合。现在所有这些权力的集合确实是一个幺半群,“乘积×被内函子的组合取代,单位由恒等函子集”。k
f^k = f(f(...))
f
k=0
f^0 = id
S
k>=0
但是:
S
可以定义为任何函子f
,甚至可以字面上定义为 的任何自映射X
。它是由 生成的幺半群f
。S
无关。f
为了让事情变得更加混乱,“幺半群中的幺半群”的定义在本书的后面部分出现,您可以从目录中看到。然而,理解这个概念对于理解与单子的联系是绝对关键的。
转到关于 Monoids 的第 VII 章(晚于关于 Monads 的第 VI 章),我们发现所谓的严格 monoidal 范畴的定义为三元组(B, *, e)
,其中B
是一个范畴,*: B x B-> B
一个双函子(关于每个分量的函子,其他分量固定) 并且是 中的单位对象,满足结合律和单位定律:e
B
(a * b) * c = a * (b * c)
a * e = e * a = a
对于 的任何对象a,b,c
,对于任何被替换为的B
态射的相同恒等式的恒等态射。现在观察到,在我们感兴趣的案例中,具有作为态射的自然变换、函子组合和恒等函子的内函子类别在哪里是有启发性的,所有这些定律都得到满足,可以直接验证。a,b,c
e
id_e
e
B
X
*
e
本书之后是“松弛”幺半群类别的定义,其中定律仅对满足所谓的相干关系的一些固定自然变换进行模数运算,但这对于我们的内函子类别并不重要。
最后,在第七章的第 3 节“Monoids”中,给出了实际的定义:
幺半群
c
中的幺半群是一个带有两个箭头(B, *, e)
的对象(态射)B
mu: c * c -> c
nu: e -> c
使3个图可交换。回想一下,在我们的例子中,这些是内函子范畴中的态射,它们是精确地对应于单子的自然join
变换return
。当我们使组合*
更明确时,联系变得更加清晰,替换c * c
为c^2
,c
我们的 monad 在哪里。
最后,请注意 3 个交换图(在幺半群类别中的幺半群定义中)是为一般(非严格)幺半群类别编写的,而在我们的例子中,作为幺半群类别的一部分出现的所有自然变换实际上都是恒等式。这将使图表与单子定义中的图表完全相同,从而使对应关系完整。
总之,根据定义,任何单子都是一个内函子,因此是内函子类别中的一个对象,其中单子join
和return
运算符满足特定(严格)幺半群类别中幺半群的定义。反之亦然,根据定义,内函子类中的任何幺半群都是由(c, mu, nu)
一个对象和两个箭头组成的三元组,例如在我们的例子中的自然变换,满足与单子相同的定律。
最后,请注意(经典)幺半群与幺半群类别中更一般的幺半群之间的主要区别。上面的两个箭头不再是二元运算和集合中的一个单位mu
。nu
相反,您有一个固定的 endofunctor c
。函子组合*
和恒等函子本身并不能提供 monad 所需的完整结构,尽管书中有令人困惑的评论。
另一种方法是与C
集合 的所有自映射的标准幺半群进行比较A
,其中二元运算是组合,可以看出将标准笛卡尔积映射C x C
到C
。传递给分类的幺半群,我们将笛卡尔积替换x
为函子组合*
,二元运算被替换为mu
从
c * c
to的自然变换c
,即join
运算符的集合
join: c(c(T))->c(T)
对于每个对象T
(在编程中键入)。经典幺半群中的恒等元素,可以用来自固定点集的地图图像来识别,被return
运算符的集合所取代
return: T->c(T)
But now there are no more cartesian products, so no pairs of elements and thus no binary operations.
我来到这篇文章是为了更好地理解 Mac Lane 的工作数学家类别理论中臭名昭著的引用的推论。
在描述某物是什么时,描述它不是什么通常同样有用。
Mac Lane 使用描述来描述 Monad 的事实可能暗示它描述了 monad 独有的东西。忍受我。为了更广泛地理解该陈述,我认为需要明确他不是在描述单子独有的东西;该声明同样描述了 Applicative 和 Arrows 等。出于同样的原因,我们可以在 Int 上拥有两个幺半群(Sum 和 Product),我们可以在 X 上拥有几个属于内函子类别的幺半群。但还有更多的相似之处。
Monad 和 Applicative 都符合标准:
(例如,在 day to dayTree a -> List b
中,但在 Category 中Tree -> List
)
Tree -> List
,只有List -> List
。该语句使用“Category of ...”这定义了语句的范围。例如,Functor Category 描述了 的范围f * -> g *
,即Any functor -> Any functor
,例如,Tree * -> List *
或Tree * -> Tree *
。
分类语句未指定的内容描述了允许任何事物的位置。
在这种情况下,在函子内部,没有指定* -> *
aka ,这意味着. 当我的想象力跳到 Int -> String 时,它还包括,甚至是where 。 a -> b
Anything -> Anything including Anything else
Integer -> Maybe Int
Maybe Double -> Either String Int
a :: Maybe Double; b :: Either String Int
所以声明如下:
:: f a -> g b
(即,任何参数化类型到任何参数化类型):: f a -> f b
(即,任何一种参数化类型到相同的参数化类型)......不同的说法,那么,这个结构的力量在哪里呢?为了欣赏完整的动态,我需要看到一个幺半群的典型绘图(带有一个标识箭头的单个对象:: single object -> single object
),未能说明我被允许使用一个带有任意数量的幺半群值参数化的箭头,来自Monoid 中允许的一种类型对象。endo, ~ 等价的标识箭头定义忽略了函子的类型值以及最内层“有效负载”层的类型和值。因此,等价true
在函数类型匹配的任何情况下返回(例如,Nothing -> Just * -> Nothing
等价于Just * -> Just * -> Just *
因为它们都是Maybe -> Maybe -> Maybe
)。
侧边栏: ~ 外部是概念性的,但它是 中最左边的符号f a
。它还描述了“Haskell”首先读入的内容(大图);所以类型相对于类型值是“外部”的。编程中层之间的关系(引用链)在 Category 中不容易关联。Set 的类别用于描述类型(Int、Strings、Maybe Int 等),其中包括 Functor 的类别(参数化类型)。引用链:Functor 类型、Functor 值(该 Functor 集合的元素,例如 Nothing、Just),以及每个 functor 值指向的其他所有内容。在 Category 中,关系被不同地描述,例如,return :: a -> m a
被认为是从一个 Functor 到另一个 Functor 的自然转换,与迄今为止提到的任何内容都不同。
回到主线,总而言之,对于任何定义的张量积和中性值,该语句最终描述了一个从其矛盾结构中诞生的惊人强大的计算结构:
:: List
);静止的fold
这没有说明有效载荷)在 Haskell 中,澄清语句的适用性很重要。这种构造的强大功能和多功能性与 monad本身完全无关。换句话说,该构造不依赖于使 monad 独一无二的原因。
当试图弄清楚是否构建具有共享上下文的代码以支持相互依赖的计算,而不是可以并行运行的计算时,这个臭名昭著的声明,尽管它描述的那样多,但并不是选择Applicative,Arrows 和 Monads,而是描述它们有多少相同。对于手头的决定,该声明没有实际意义。
这常常被误解。该声明继续描述join :: m (m a) -> m a
为单曲面内函子的张量积。但是,它没有明确说明在本声明的上下文中(<*>)
也可以如何选择。这确实是六/六打的一个例子。组合值的逻辑完全相同;相同的输入从每个生成相同的输出(与 Int 的 Sum 和 Product 幺半群不同,因为它们在组合 Int 时会生成不同的结果)。
因此,回顾一下:内函子类别中的一个幺半群描述:
~t :: m * -> m * -> m *
and a neutral value for m *
(<*>)
并且(>>=)
两者都提供对两个值的同时访问m
,以便计算单个返回值。用于计算返回值的逻辑完全相同。如果不是因为它们参数化的函数的不同形状(f :: a -> b
与k :: a -> m b
)以及具有相同计算返回类型的参数的位置(即,分别a -> b -> b
对b -> a -> b
每个),我怀疑我们可以参数化幺半群逻辑,张量积,用于在两个定义中重用。作为一个练习来说明这一点,尝试并实施~t
,你最终会得到(<*>)
并(>>=)
取决于你决定如何定义它forall a b
。
如果我的最后一点在概念上至少是正确的,那么它就解释了 Applicative 和 Monad 之间精确且唯一的计算差异:它们参数化的函数。换句话说,差异在这些类型类的实现之外。
总之,根据我自己的经验,Mac Lane 臭名昭著的名言提供了一个很好的“goto”模因,这是我在浏览 Category 以更好地理解 Haskell 中使用的习语时参考的路标。它成功地捕捉到了在 Haskell 中非常容易访问的强大计算能力的范围。
然而,具有讽刺意味的是,我首先误解了该声明在 monad 之外的适用性,以及我希望在这里传达的内容。它所描述的一切都证明是 Applicative 和 Monads(以及 Arrows 等)之间的相似之处。它没有说的正是它们之间微小但有用的区别。
-E
注意:不,这不是真的。在某些时候,丹·皮波尼本人对这个答案发表了评论,他说这里的因果关系完全相反,他写这篇文章是为了回应詹姆斯·艾里的俏皮话。但它似乎已被删除,也许是一些强迫性的整理者。
以下是我的原始答案。
Iry 很可能读过From Monoids to Monads,一篇文章 Dan Piponi (sigfpe) 从 Haskell 中的 monoids 派生了 monad,其中对范畴论进行了很多讨论,并明确提到了“Hask 上的内函子范畴”。无论如何,任何想知道单子成为内函子类别中的幺半群意味着什么的人都可能从阅读这个推导中受益。