Monad理论和Haskell

大多数教程似乎给了monads(IO,状态,列表等等)的很多例子,然后期望读者能够抽象出整体原理,然后他们提到类别理论。 我并不倾向于通过从例子中泛化来学习,我想从理论的angular度来理解为什么这个模式如此重要。

从这个线程判断: 任何人都可以解释Monads? 这是一个常见的问题,我已经尝试了大部分的教程(除了Brian Beckvideo,不会在我的Linux机器上播放):

有没有人知道从类别理论开始的教程,并解释IO,状态,列表monad这些条款? 以下是我不成功的尝试:

据我所知,一个monad包含一个三元组:一个内部函子和两个自然转换。

函子通常用types表示:(a – > b) – >(ma – > mb)为了强调对称性,我包含了第二个括号。

但是,这是一个pipe理者的终结,所以不应该像这样的域和共域吗?

(a→b)→(a→b)

我认为答案是域和共域都有一个types:

(a – > b)| (ma – > mb)| (mma – > mmb)等等…

但是我不确定这是否符合给定函子的定义?

当我们转向自然变革时,情况会变得更糟。 如果我理解正确的话,一个自然变换就是一个二次仿函数(具有一定的规则),它是一个仿函数的仿函数。 因此,由于我们已经定义了上面的函子,所以自然变换的一般types是:(a→b)→(ma→mb)→→(a→b)→ma→mb ))

但是我们正在使用的实际的自然转换有types:

a – > ma

ma – >(a – > mb) – > mb

上述一般forms的这些子集? 为什么他们是自然的转变?

马丁

一个快速的免责声明:一般来说,我对分类理论有点不稳定,但我觉得你至less有一些熟悉的地方。 希望我不会做太多的这个…

有没有人知道从类别理论开始的教程,并解释IO,状态,列表monad这些条款?

首先,现在忽略IO ,它充满了黑暗的魔力。 由于State为有状态计算build模工作的相同原因,它作为命令式计算的模型工作,但与后者不同, IO是无法从外部推断一元结构的黑盒子。

函子通常用types表示:(a – > b) – >(ma – > mb)为了强调对称性,我包含了第二个括号。

但是,这是一个pipe理者的终结,所以不应该像这样的域和共域吗?

我怀疑你错误地解释了Haskell中的typesvariables如何与类别理论概念相关联。

首先,是的,它指定了一个基于Haskelltypes的endofunctor。 然而,typesvariables(如a )在这个类别中并不是什么东西, 它是一个variables(隐含地)在范畴中的所有对象上被普遍量化。 因此,types(a -> b) -> (a -> b)只描述将每个对象映射到自身的endofunctor

types构造函数描述对象的一个​​内射函数,其中构造函数的codomain的元素除了作为types构造函数的应用之外不能用任何方式描述。 即使两个types的构造函数产生同构结果,结果types仍然是不同的。 请注意,在一般情况下,types构造函数不是函子。

然后,函子签名中的typesvariablesm表示一个参数types的构造函数。 在这种情况下,这通常被认为是普遍的量化,但在这种情况下这是不正确的,因为不存在这样的function。 相反,类的类定义绑定m并允许为特定的types构造函数定义这些函数。

所得到的函数表明,对于任何具有fmap定义的types构造函数m ,对于任意两个对象ab以及它们之间的态射,我们可以在通过对ab应用m给出的types之间find一个态射。

请注意,虽然上面的确确定了哈斯克的一位pipe理者 ,但是对于所有这样的pipe理者来说 ,它甚至不足以描述它们。

但是我们正在使用的实际的自然转换有types:

a – > ma

ma – >(a – > mb) – > mb

上述一般forms的这些子集? 为什么他们是自然的转变?

那么,不,他们不是。 自然变换大致是函数之间的一个函数(不是函子)。 指定单子M的两个自然转换看起来像I -> M ,其中I是身份函数, M ∘ M -> M ,其中是函子的组成。 在Haskell中,我们没有直接使用真正的身份函子函子组合的好方法。 相反,我们放弃了身份函子,第一次得到(Functor m) => a -> ma ,第二次写出嵌套types的构造函数为(Functor m) => m (ma) -> ma

其中第一个显然是return ; 第二个是一个名为join的函数,它不是types的一部分。 然而, join可以用(>>=) ,后者在日常编程中更常用。


至于具体的monad去,如果你想要一个更加math的描述,这里是一个例子的简要概述:

对于某些固定typesS,考虑两个函数F和G,其中F(x)=(S,x)和G(x)= S – > x(希望这些函数确实是有效函数应该是显而易见的)。

这些函数也是伴随的; 考虑自然变换unit :: x -> G (F x)counit :: F (G x) -> x 。 扩展定义给出了unit :: x -> (S -> (S, x))counit :: (S, S -> x) -> x types提出了不安全的函数应用和元组构造; 随时validation那些工作如预期。

一个函数由一个函子组成,产生一个单子,所以取G∘F并扩展定义,得到G(F x)= S – >(S,x),它是State单子的定义。 附加unit当然是return ; 你应该可以使用counit来定义join

这个页面完全一样。 我认为你的主要困惑是,类没有真正使types的函数,但它定义了一个从Haskelltypes的类函数到types的类别。

按照链接的符号,假设F是一个Haskell函子,这意味着有一个从Hask类到F类的函子。

粗略地说,Haskell只在一个类中做类别理论,其对象是Haskelltypes,其箭头是这些types之间的函数。 这绝对不是用于build模类别理论的通用语言。

一个(math)函数是一个把一个类别的东西转换成另一个可能完全不同的类别的东西。 然后endofunctor是一个仿函数,碰巧有相同的源和目标类别。 在Haskell中,一个函子是一种把Haskelltypes的东西变成Haskelltypes的东西,所以它总是一个endofunctor。

(a-> b) – >(ma – > mb)'只是内核函数m的箭头部分 ,'m'是目标部分 ]

当哈斯克勒谈论“在单子中”的工作时,他们确实是指在单子的克莱斯里类别中工作。 一个monad的Kleisli类别首先是一个彻底混淆的野兽,通常需要至less两种颜色的墨水来给出一个很好的解释,所以下面的尝试是什么和检查一些参考(很遗憾,维基百科在这里是无用的除了直接的定义外)。

假设你在Haskelltypes的类别C上有一个monad'm'。 它的Kleisli范畴Kl(m)与C有相同的对象,即Haskelltypes,但是Kl(m)中的箭头a〜(f)〜b是C中的箭头a-(f) – > mb。在我的Kleisli箭头中用了一条波浪线来区分两者)。 重申:Kl(C)的物体和箭头也是C的物体和箭头,但是箭头指向Kl(C)中的不同物体而不是C中的物体。如果这不会使你觉得奇怪,请再阅读一遍小心!

具体来说,考虑Maybe monad。 它的Kleisli类只是Haskelltypes的集合,它的箭头a〜(f)〜> b是函数a – (f) – >也许b。 或者考虑一下(状态s)monad,其箭头a〜(f)〜b是函数a-(f) – >(state sb)== a-(f) – >(s – >(s,b)) 。 无论如何,你总是写一个扭曲的箭头作为你的函数共域的types的简写。

[请注意,状态不是单子,因为状态的types是* – > * – > *,所以您需要提供其中一个types参数以将其变成math单子。]

希望如此好,但是假设你想组成箭头a〜(f)〜> b和b〜(g)〜> c。 这些都是真正的Haskell函数a – (f) – > mb和b – (g) – > mc,因为types不匹配,所以您不能编写。 math解决scheme是使用monad的“乘法”自然变换u:mm-> m如下:a〜(f)〜> b〜(g)〜> c == a – (f) – > mb – (mg) – > mmc – (uc) – > mc,得到箭头a-> mc,这是一个Kleisli箭头a〜(f; g)〜> c。

也许在这里有一个具体的例子。 在Maybe monad中,你不能编写函数f:a – > Maybe b和g:b – >可能直接c,但是通过提起g来

 Maybe_g :: Maybe b -> Maybe (Maybe c) Maybe_g Nothing = Nothing Maybe_g (Just a) = Just (ga) 

并使用“明显的”

 u :: Maybe (Maybe c) -> Maybe c u Nothing = Nothing u (Just Nothing) = Nothing u (Just (Just c)) = Just c 

你可以组成u . Maybe_g . f u . Maybe_g . f u . Maybe_g . f这是函数a – >也许c你想要的。

在(状态)monad中,它是类似的,但更加混乱:给定两个一元函数a〜(f)〜> b和b〜(g)〜> c,它们实际上是一个 – (f) – >(s – > ,b))和b – (g) – >(s – >(s,c)),

 State_s_g :: (s->(s,b)) -> (s->(s,(s->(s,c)))) State_s_g p s1 = let (s2, b) = p s1 in (s2, gb) 

那么你应用了“乘法”自然变换u,这是

 u :: (s->(s,(s->(s,c)))) -> (s->(s,c)) u p1 s1 = let (s2, p2) = p1 s1 in p2 s2 

哪种(哪种)把f的最终状态插入g的初始状态。

在Haskell中,事实certificate这是一种不自然的工作方式,所以它有(>>=)函数,这个函数基本上与u相同,但是使用起来更方便。 这很重要: (>>=)不是自然转换“u”。 你可以用另一个来定义每一个,所以它们是相同的,但它们不是一回事。 Haskell版本的“u”被写入join

这个Kleisli范畴的定义中缺less的另一件事是每个对象的身份:a(1_a)〜> a其实是一个 – (n_a) – > ma,其中n是单位的自然变换。 这是在Haskell写return ,似乎并没有造成太多的混淆。

在我来到Haskell之前,我学到了类别理论,而且我也对math家称之为单子之间的不匹配以及他们在Haskell中看起来像什么有些困难。 从另一个方向来看并不容易!

不知道我明白什么是问题,但是,是的,你说得对,哈斯克尔monad被定义为三重:

 m :: * -> * -- this is endofunctor from haskell types to haskell types! return :: a -> ma (>>=) :: ma -> (a -> mb) -> mb 

但类别理论的普遍定义是另外一个三元组:

 m :: * -> * return :: a -> ma join :: m (ma) -> ma 

这有点混淆,但并不难说明这两个定义是相同的。 为此,我们需要根据(>>=)定义join (反之亦然)。 第一步:

 join :: m (ma) -> ma join x = ? 

这给了我们x :: m (ma)
我们所能做的所有types为m _东西就是aply(>> =):

 (x >>=) :: (ma -> mb) -> mb 

现在我们需要一些东西作为(>> =)的第二个参数,而且根据连接的types,我们有约束(x >>= y) :: ma
所以在这里你会得到typesy :: ma -> maid :: a -> a很适合:

 join x = x >>= id 

另一种方法

 (>>=) :: ma -> (a -> mb) -> mb (>>=) xy = ? 

其中x :: may :: a -> mb 。 为了从xy得到mb ,我们需要一些types为a东西。
不幸的是,我们无法从ma提取a 。 但是我们可以用它替代别的东西(记住,monad也是一个仿函数):

 fmap :: (a -> b) -> ma -> mb fmap yx :: m (mb) 

而且它非常适合作为连接的参数: (>>=) xy = join (fmap yx)

查看monad和计算效果的最好方法是从Haskell得到monads的计算效果的概念开始,然后在了解之后查看Haskell。 尤其请参阅本文:E. Moggi的“计算和Monads的概念” 。

另请参见Moggi早期的文章,它显示单子如何为lambda演算单独工作: http ://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.2787

monads捕获替代的事实,以及替代是lambda演算的关键,应该给一个很好的线索,为什么他们有这么多的performance力。

虽然monads最初来自类别理论,但这并不意味着类别理论是您可以查看它们的唯一的抽象背景。 操作语义给出了一个不同的观点。 有关介绍,请查看我的Operational Monad教程 。

看待IO的一种方法是将其视为一种奇怪的状态monad。 请记住,monad状态看起来像:

 data State sa = State (s -> (s, a)) 

其中“s”参数是要通过计算进行线程化的数据types。 另外,这个版本的“State”没有“get”和“put”动作,我们不会导出构造函数。

现在想象一下types

 data RealWorld = RealWorld ...... 

这没有真正的定义,但是从理论上来说,RealWorldtypes的值保存了整个计算机外部的状态。 当然,我们永远不可能拥有RealWorldtypes的价值,但是您可以想象如下:

 getChar :: RealWorld -> (RealWorld, Char) 

换句话说,“getChar”函数在按下键盘button之前获取宇宙状态,并在按下按键之后返回按下的键加上宇宙的状态。 当然问题是,世界的前一个状态仍然可以被引用,而这在现实中是不可能发生的。

但现在我们写这个:

键入IO =状态RealWorld

getChar :: IO Char

从理论上讲,我们所做的一切就是将以前版本的“getChar”作为状态动作。 但是通过这样做,我们不能再访问“RealWorld”的值,因为它们被封装在State monad中。

所以当一个Haskell程序想要改变一个灯泡的时候,它会占用灯泡,并在IO内的RealWorld值上应用一个“旋转”函数。

对我而言,到目前为止,最接近把类别理论中的单子和哈斯克尔中的单子联系起来的解释是,单子是一个monid,其对象的types是a-> m b。 我可以看到,这些对象非常接近pipe理者,所以这些function的组成与程序语句的命令序列有关。 另外返回IO函数的函数在纯函数代码中是有效的,直到从外部调用内部函数为止。

这个id元素是非常适合的“a – > ma”,但乘法元素是函数组成,它应该是:

(> =>):: Monad m =>(a – > mb) – >(b – > mc) – >(a – > mc)

这不是完全的函数组合,但足够接近(我认为要得到真正的函数组合,我们需要一个互补的函数,把mb变回a,然后我们得到函数组合,如果我们成对地应用这些)?我不太确定如何从这个到这个:

(>> =):: Monad m => ma – >(a – > mb) – > mb

我有一种感觉,我可能已经在所有阅读过的东西中看到了这个解释,但是第一次没有了解它的意义,所以我会做一些重读,试着(重新)find这个解释。

我想做的另一件事是把所有不同的范畴理论解释联系起来:endofunctor + 2自然转换,Kleisli范畴,monoid对象是monids等等。 对我来说,似乎把所有这些解释联系在一起的东西是他们两个层面。 也就是说,通常我们将类别对象视为黑盒子,在这里我们暗示他们的属性来自外部的相互作用,但是在这里似乎需要在对象内部进行一个层次来看看发生了什么。 我们可以解释monad没有这个,但只有当我们接受显然任意的构造。

马丁

看到这个问题: 链接操作是monad类解决的唯一事情吗?

在这里,我解释一下我的观点:我们必须区分Monad类和解决个体问题的个体types。 Monad类本身只解决了“select性链接操作”这一重要问题,并通过“inheritance”的方式使这种解决scheme成为实例types。

另一方面,如果解决给定问题的给定types面临“select性链接操作”的问题,则应该将其作为Monad类的实例(inheritance)。

事实上,问题不仅仅是作为一个Monad来解决。 这就好像说“轮子”解决了很多问题,但实际上“轮子”只能解决问题,带轮子的问题解决了很多不同的问题。