haskell 单子只是内函子范畴中的一个幺半群,有什么问题呢?

ej83mcc0  于 2022-11-14  发布在  其他
关注(0)|答案(5)|浏览(145)

下面谁先说的?
单子只是内函子范畴中的一个幺半群,有什么问题呢?
还有一个不太重要的问题,这是真的吗?如果是真的,你能给予一个解释吗?(希望一个没有太多Haskell经验的人能理解)

k10s72fa

k10s72fa1#

这句话出自詹姆斯·艾里(James Iry)之手,出自他极具娱乐性的 * Brief, Incomplete and Mostly Wrong History of Programming Languages *,他在书中虚构地将其归功于菲利普·瓦德勒(Philip Wadler)。
最初的引文来自桑德斯·麦克莱恩(Saunders Mac Lane)在《工作数学家的范畴》(Categories for the Working Mathematician)一书中的话,这是范畴论的基础性著作之一,在这里,我们可以从上下文中了解它的确切含义。
但是,我会尝试一下。原文是这样的:
总之,X中的单子只是X的内函子范畴中的一个幺半群,乘积×被内函子的合成所取代,单位集被单位内函子所取代。
这里X是一个范畴,内函子是从一个范畴到它自身的函子(对于函数程序员来说,这通常是所有的函子,因为他们大多数时候只处理一个范畴;类型的范畴--但我离题了)。2但你可以想象另一个范畴是“X上的内函子”的范畴。3这是一个范畴,其中的对象是内函子,态射是自然变换。
在这些内函子中,有一些可能是单子。哪些是单子?在特定意义上是 monoidal 的那些。我不想详细说明从单子到单子的Map(因为Mac Lane做得比我希望的要好得多),我只是把它们各自的定义放在一起,让你比较一下:
幺半群是...

  • 一套,S
  • 手术,***·:S × S → S***
  • Se的一个元素:1 → S

...满足这些定律:

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

单子是...

  • 一个内函子,T:X → X(在Haskell中,* -> *类型的类型构造函数,带有Functor示例)
  • 自然变换,μ:T × T → T,其中 × 表示函子复合(μ 在Haskell中称为 * join *)
  • 一个自然变换,η:I → T,其中 IX 上的单位内函子(η 在Haskell中称为 * return *)

...满足这些定律:

  • μ Tμ = μ μT
  • μ Tη = μ ηT = 1(恒等自然变换)

稍微眯一下眼睛,您可能会看到这两个定义都是同一个abstract concept的示例。

9q78igpj

9q78igpj2#

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

{-# LANGUAGE RankNTypes, TypeOperators #-}

import Control.Monad (join)

其中,RankNTypes是唯一一个对下面的内容绝对必要的,我曾经写过一个关于RankNTypes的解释,有些人似乎发现它很有用,所以我会引用它。
引用Tom Crockett's excellent answer,我们有:
单子是...

  • 一个内函子,T:X -〉X
  • 自然变换,μ:T × T -〉T,其中 × 表示函子复合
  • 一个自然变换,η:I -〉T,其中 IX 上的单位函子

...满足这些定律:

  • μ(μ(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”。Haskell中的每个Functor都是人们称之为“Hask范畴”的内函子,其对象是Haskell类型(*),且其态射是 haskell 函数。这听起来像是一个复杂的陈述,但实际上这是一个非常琐碎的问题。这意味着Functor f :: * -> *提供了为任何a :: *构造类型f a :: *和从任何f :: a -> b构造函数fmap f :: f a -> f b的方法,并且它们服从函子律。
第二条:Haskell中的Identity函子(随Platform一起提供,因此您可以直接导入它)是这样定义的:

newtype Identity a = Identity { runIdentity :: a }

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

所以自然变换***η:对于任何Monad示例t,Tom克罗克特定义中的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)

所以自然变换***μ: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

这些都很容易证明,因为ComposeIdentity都被定义为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.
hivapdat

hivapdat3#

The answers here do an excellent job in defining both monoids and monads, however, they still don't seem to answer the question:
And on a less important note, is this true and if so could you give an explanation (hopefully one that can be understood by someone who doesn't have much Haskell experience)?
The crux of the matter that is missing here, is the different notion of "monoid", the so-called categorification more precisely -- the one of monoid in a monoidal category. Sadly Mac Lane's book itself makes it very confusing:
All told, a monad in X is just a monoid in the category of endofunctors of X , with product × replaced by composition of endofunctors and unit set by the identity endofunctor.

Main confusion

Why is this confusing? Because it does not define what is "monoid in the category of endofunctors" of X . Instead, this sentence suggests taking a monoid inside the set of all endofunctors together with the functor composition as binary operation and the identity functor as a monoidal unit. Which works perfectly fine and turns into a monoid any subset of endofunctors that contains the identity functor and is closed under functor composition.
Yet this is not the correct interpretation, which the book fails to make clear at that stage. A Monad f is a fixed endofunctor, not a subset of endofunctors closed under composition. A common construction is to use f to generate a monoid by taking the set of all k -fold compositions f^k = f(f(...)) of f with itself, including k=0 that corresponds to the identity f^0 = id . And now the set S of all these powers for all k>=0 is indeed a monoid "with product × replaced by composition of endofunctors and unit set by the identity endofunctor".
And yet:

  • This monoid S can be defined for any functor f or even literally for any self-map of X . It is the monoid generated by f .
  • The monoidal structure of S given by the functor composition and the identity functor has nothing do with f being or not being a monad.

And to make things more confusing, the definition of "monoid in monoidal category" comes later in the book as you can see from the table of contents. And yet understanding this notion is absolutely critical to understanding the connection with monads.

(Strict) monoidal categories

Going to Chapter VII on Monoids (which comes later than Chapter VI on Monads), we find the definition of the so-called strict monoidal category as triple (B, *, e) , where B is a category, *: B x B-> B a bifunctor (functor with respect to each component with other component fixed) and e is a unit object in B , satisfying the associativity and unit laws:

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

for any objects a,b,c of B , and the same identities for any morphisms a,b,c with e replaced by id_e , the identity morphism of e . It is now instructive to observe that in our case of interest, where B is the category of endofunctors of X with natural transformations as morphisms, * the functor composition and e the identity functor, all these laws are satisfied, as can be directly verified.
What comes after in the book is the definition of the "relaxed" monoidal category, where the laws only hold modulo some fixed natural transformations satisfying so-called coherence relations, which is however not important for our cases of the endofunctor categories.

Monoids in monoidal categories

Finally, in section 3 "Monoids" of Chapter VII, the actual definition is given:
A monoid c in a monoidal category (B, *, e) is an object of B with two arrows (morphisms)

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

making 3 diagrams commutative. Recall that in our case, these are morphisms in the category of endofunctors, which are natural transformations corresponding to precisely join and return for a monad. The connection becomes even clearer when we make the composition * more explicit, replacing c * c by c^2 , where c is our monad.
Finally, notice that the 3 commutative diagrams (in the definition of a monoid in monoidal category) are written for general (non-strict) monoidal categories, while in our case all natural transformations arising as part of the monoidal category are actually identities. That will make the diagrams exactly the same as the ones in the definition of a monad, making the correspondence complete.

Conclusion

In summary, any monad is by definition an endofunctor, hence an object in the category of endofunctors, where the monadic join and return operators satisfy the definition of a monoid in that particular (strict) monoidal category. Vice versa, any monoid in the monoidal category of endofunctors is by definition a triple (c, mu, nu) consisting of an object and two arrows, e.g. natural transformations in our case, satisfying the same laws as a monad.

最后,请注意(经典)幺半群和幺半群范畴中更一般的幺半群。上面的两个箭头munu不再是二元运算和集合中的单位。相反,你有一个固定的内函子c。函子复合*和单位函子本身并不提供单子所需的完整结构,尽管书中有令人困惑的注解。
另一种方法是与集合A的所有自Map的标准幺半群C进行比较,其中二元运算是合成,可以看到它将标准笛卡尔积C x CMap到C。转到分类幺半群,我们用函子合成*替换笛卡尔积x。并且二元运算被从x1M57n1x到x1M58n1x的自然变换x1M56n1x所替换,该自然变换是x1M59n1x运算符的集合,

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

对于每个对象T(程序设计中的类型),用return算子的集合来代替经典幺半群中的单位元,这些单位元可以用一个固定单点集上的Map的图像来识别

return: T->c(T)

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

kqqjbcuj

kqqjbcuj4#

我之所以写这篇文章,是为了更好地理解麦克·莱恩(Mac Lane)的《工作数学家的范畴论》(Category Theory For the Working Mathematician)中那句臭名昭著的话的推论。
在描述某物是什么的时候,描述它不是什么通常同样有用。
事实上,Mac Lane使用这个描述来描述单子,这可能意味着它描述了单子所独有的东西。请耐心听我说。为了更广泛地理解这个陈述,我认为需要澄清的是,他 * 不是 * 描述了单子所独有的东西;这个陈述同样地描述了应用和箭头等。2由于同样的原因,我们可以在Int上有两个幺半群(和和积),我们可以在X上的内函子范畴中有几个幺半群。3但是,它们之间的相似之处更多。
Monad和Appliative均符合标准:

  • endo =〉任何在同一位置开始和结束的箭头或态射
  • 函子=〉任意箭头,或两个范畴之间态射

(e.g.,每天Tree a -> List b,但类别Tree -> List

  • 幺半群=〉单一对象;即单一类型,但在本文中,仅涉及外层;所以,我们不能有Tree -> List,只能有List -> List

该语句使用“Category of...”,这定义了语句的作用域。例如,函子类别描述f * -> g *的作用域,即Any functor -> Any functor,例如Tree * -> List *Tree * -> Tree *
一个分类陈述没有指定的东西描述了在什么地方 * 任何事情和一切都是允许的 *。
在这个例子中,函子内部没有指定* -> *,也就是a -> b,这意味着Anything -> Anything including Anything else。当我的想象力跳到Int -〉String时,它也包括Integer -> Maybe Int,甚至Maybe Double -> Either String Int,其中a :: Maybe Double; b :: Either String Int
因此,该语句组合如下:

  • 函子作用域:: f a -> g b(即,任何参数化类型到任何参数化类型)
  • endo +函子:: f a -> f b(即任何一个参数化类型到同一个参数化类型)......换句话说,
  • 内函子范畴中的幺半群

那么,这个构造的力量在哪里呢?为了欣赏完整的动力学,我需要看到幺半群的典型图形(单个对象,看起来像一个标识箭头,:: single object -> single object),未能说明我被允许从Monoid中允许的 * 一个 * 类型对象中,使用 * 任意数量 * 的Monoid值参数化的箭头。等价的~ identity箭头定义 * 忽略 * 函子的 * 类型值 * 以及最内部的“有效负载”层的类型和值。因此,在函子类型匹配的任何情况下,等价返回true(例如,Nothing -> Just * -> Nothing等于Just * -> Just * -> Just *,因为它们都是Maybe -> Maybe -> Maybe)。
侧边栏:~ outside是概念性的,但它是f a中最左边的符号。它也描述了“Haskell”首先读入的内容(大图片);所以类型相对于类型值是“外部的”。编程中的层之间的关系(引用链)不容易在范畴中联系起来。集合范畴用于描述类型(Int,String,Maybe Int等),它包括函子范畴(参数化类型)。引用链:函子类型、函子值(该函子集合的元素,例如Nothing、Just),以及每个函子值所指向的其他一切。在范畴中,关系被不同地描述,例如,return :: a -> m a被认为是从一个函子到另一个函子的自然变换,不同于迄今为止提到的任何东西。
回到主线上,总而言之,对于任何定义的Tensor积和一个中性值,这个陈述最终描述了一个从其悖论结构中产生的令人惊讶的强大计算构造:

  • 在外部,它表现为单个对象(例如,:: List);静态的
  • 但在内部,允许很多动态
  • 任意数量的相同类型的值(例如,Empty| ~NonEmpty)作为任意arity函数的素材。Tensor积会将任意数量的输入减少为单个值...用于外层(~ fold,它对有效载荷没有任何意义)
  • 最内层的类型和值的无限范围

在Haskell中,阐明陈述的适用性是很重要的。这个构造的能力和多功能性与单子本身完全无关。换句话说,这个构造不依赖于单子的唯一性。
当试图弄清楚是用共享上下文来构建代码以支持相互依赖的计算,还是可以并行运行的计算时,这个臭名昭著的陈述,正如它所描述的那样,并不是在选择应用型、箭头型和单子型之间进行对比,而是在描述它们有多少相同。对于手头的决定,这个陈述是没有意义的。

这经常被误解。该陈述接着描述join :: m (m a) -> m a为幺正内函子的Tensor积。然而,它没有阐明在该陈述的上下文中,(<*>)如何也可以被选择。它确实是“一个中有六个,另一个中有半打”的例子。组合值的逻辑是完全相似的;相同的输入会从每个输入生成相同的输出(与Int的Sum和Product幺半群不同,因为它们在组合Int时会生成不同的结果)。
所以,我们来总结一下:内函子范畴中的幺半群描述了:

~t :: m * -> m * -> m *
 and a neutral value for m *

(<*>)(>>=)都提供对两个m值的同时访问,以便计算单个返回值。用于计算返回值的逻辑完全相同。如果不是因为它们参数化的函数的形状不同,(f :: a -> bk :: a -> m b)和具有相同计算返回类型的参数的位置(即,分别为a -> b -> bb -> a -> b),我怀疑我们可以将幺半群逻辑,Tensor积参数化,以便在两个定义中重用。作为说明这一点的练习,尝试实现~t,最终将得到(<*>)(>>=),这取决于您决定如何定义它forall a b
如果我的最后一点至少在概念上是正确的,那么它就解释了应用型和单子型之间精确的、唯一的计算上的区别:换句话说,差异是这些类型类的实现的 * 外部 *。
最后,根据我的经验,麦克·莱恩那句臭名昭著的名言为我提供了一个很好的“后藤”模因,一个指引我在浏览类别时参考的路标,以便更好地理解Haskell中使用的习语。它成功地捕捉到了Haskell中令人惊叹的强大计算能力的范围。
然而,讽刺的是,我一开始误解了这句话在单子之外的适用性,也误解了我希望在这里表达的意思。它所描述的一切都是应用型和单子(以及箭头等)之间的相似之处。它没有说的正是它们之间微小但有用的区别。

k4aesqcs

k4aesqcs5#

  • 注:* 不,这不是真的。在某个时候,丹·皮波尼自己对这个答案发表了评论,说这里的因果关系完全相反,他写这篇文章是为了回应詹姆斯·伊里的俏皮话。但似乎已经被删除了,也许是被一些强迫性的整理者删除了。

以下是我最初的回答。
Iry很有可能读过一篇文章From Monoids to Monads,其中Dan Piponi(sigfpe)在Haskell中从幺半群推导出了单子,文章中有很多关于范畴论的讨论,并明确提到了“Hask上的内函子范畴“。无论如何,任何想知道单子是内函子范畴中的幺半群意味着什么的人都可以从阅读这篇推导中受益。

相关问题