单子理论和Haskell

Question

大多数教程似乎给出了许多单子（IO、state、list等）的例子，然后期望读者能够抽象出总体原则，然后提到范畴论。我不太喜欢尝试从例子中概括学习，我希望从理论角度理解为什么这种模式如此重要。

从这个主题判断： Can anyone explain Monads? 这是一个常见的问题，我尝试查看了大多数建议的教程（除了无法在我的Linux机器上播放的Brian Beck视频）：

有没有人知道一个从范畴论开始并以这些术语解释IO、state、list monads的教程？以下是我未成功尝试所做的尝试：

据我理解，一个单子由三部分组成：一个自函子和两个自然变换。

通常用下面的类型来表示该函子： (a -> b) -> (m a -> m b) 我添加了第二个括号只是为了强调对称性。

但是，这是一个自函子，因此域和陪域应该相同，像这样吗？：

(a -> b) -> (a -> b)

我认为答案是，域和陪域都具有以下类型：

(a -> b) | (m a -> m b) | (m m a -> m m b) 等等……

但我不确定这是否有效或是否符合给定函子的定义？

当我们转向自然变换时，情况变得更糟。如果我理解正确，自然变换是一个二阶函子（具有某些规则），它是从一个函子到另一个函子的函子。因此，由于我们已经定义了上面的函子，自然变换的一般类型将是：

((a -> b) -> (m a -> m b)) -> ((a -> b) -> (m a -> m b))

但实际使用的自然变换类型为：

a -> m a

m a -> (a ->m b) -> m b

这些是通用形式的子集吗？为什么它们是自然变换？

Martin

- Martin

---

+1给一位同样是演绎学习者的朋友。与权力斗争！ - Derrick Turk

我发现“函子+2个自然变换”的观点最清晰，但对每个人来说可能并非如此。单子有不同等效定义，练习同时操作它们是很好的练习。就像任何抽象对象一样，融合定义需要时间。即使你能找到很多教程，学习单子也不会很“容易”。其作者必须与数学搏斗，就像你一样。 - Alexandre C.

但是，这是一个自函子，所以域和陪域不应该像这样相同吗？：(a -> b) -> (a -> b) -- 不是的。作为一个自函子，只意味着 m 的域和陪域（它们是范畴）应该相同，这里是 Haskell 类型的范畴。 - Alexandre C.

这里可能存在一些混淆，原因在于fmap所要求的类型签名不够一般化，无法描述所有在Hask上的自函子，只能描述所有从Hask到某个类型构造子定义的子范畴上的函子。 - C. A. McCann

Answer 1

快速免责声明：我对范畴论有点不熟悉，但我感觉你至少有一些了解。希望我不会把这个搞砸太多...

有人知道从范畴论开始，用IO、State和List Monad解释的教程吗？

首先，现在先忽略IO，它充满了黑魔法。它作为模拟命令式计算的模型，与State类似，但与后者不同的是，IO是一个黑匣子，没有办法从外部推断出单子结构。

通常用以下类型显示函子：(a->b)->(m a-> m b)，我添加了第二个括号只是为了强调对称性。

但是，这是一个恒自函子，所以定义域和值域应该相同，像这样：

我怀疑你误解了Haskell中类型变量与范畴论概念的关系。

首先，是的，这指定了Haskell类型范畴上的一个恒自函子。然而，例如a的类型变量在此范畴中并不代表任何东西，它是一个隐含地普遍量化到该范畴中所有对象上的变量。因此，类型(a -> b) -> (a -> b)仅描述“将每个对象映射到自身”的恒自函子。

类型构造函数描述了对象的单射函数，其中构造函数的值域元素不能以任何方式描述，除非作为类型构造函数的应用。即使两个类型构造函数产生同构结果，结果类型仍然是不同的。请注意，类型构造函数在一般情况下不是函子。在functor签名中，类型变量表示一个一元类型构造器。如果没有上下文，这通常会被解读为普遍量化，但在这种情况下是不正确的，因为不存在这样的函数。相反，类型类定义绑定并允许为特定类型构造器定义这样的函数。

因此，得到的函数表明，对于任何具有定义了fmap的类型构造器，对于任何两个对象和以及它们之间的态射，我们可以找到应用到和所给出的类型之间的一个态射。

请注意，虽然上述内容当然定义了上的一个自函子，但它远远不足以描述所有这样的自函子。

引用块中使用的实际自然变换的类型如下：

a -> m a

m a -> (a ->m b) -> m b

它们是否是上述通用形式的子集？它们为什么是自然变换？

实际上，它们不是。一个自然变换大致是两个函子之间的函数（而不是一个函子）。指定monad M的两个自然变换看起来像I -> M，其中I是恒等函子，以及M∘M -> M，其中∘是函子组合。在Haskell中，我们没有直接使用真正的恒等函子或函子组合的好方法。相反，我们放弃恒等函子，仅得到(Functor m) => a -> m a为第一个自然变换，并将嵌套类型构造器应用写成(Functor m) => m (m a) -> m a作为第二个自然变换。这里有两个函数，第一个显然是return; 第二个函数是一个名为 join 的函数，它不是类型类中的一部分。然而，join可以用(>>=)来表示，而且后者在日常编程中更常用。

具体的单子模式，如果你想要更数学化的描述，下面是一个例子的简单概述：

对于某个固定的类型S，考虑两个函子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。这些类型建议使用未柯里化的函数应用和元组构造；可以验证它们按预期工作。

通过组合函子，伴随产生了一个单子模式，因此取 G ∘ F 并扩展定义，我们得到 G(F x) = S -> (S, x)，这就是State monad的定义。伴随的unit当然是return；你应该能够使用counit来定义join。

- C. A. McCann

---

G也可能是单子的 - 这取决于S的定义。我在这个答案中提供了一个概述。 - atravers

Answer 2

这个页面正是做到了这一点。我认为你主要的困惑在于，该类并没有使类型成为一个函子，而是定义了从Haskell类型范畴到该类型范畴的函子。

按照链接的表示法，假设F是一个Haskell函子，则意味着有一个从Hask范畴到F范畴的函子。

- HaskellElephant

---

谢谢，这是一个有趣的页面。然而请注意注释2中所说：“有经验的范畴论者会注意到我们在这里简化了一些事情；我们将单位和结合呈现为显式的态射，要求自然性作为标准单子律（第3和第4条）之外的额外公理。”因此，他们似乎隐藏了至少一个导致我问题的问题，即将一个二范畴简化为一个一范畴。 - Martin

我会再次阅读这篇文章，并仔细思考是否有任何遗漏之处。我还会考虑一个自函子f引发Haskell函子F的想法。 - Martin

@Martin：我非常确定你不需要超过一个类别来做到一切正确。 - sclv

@Martin -- 是的，解释态射是如何来自自然变换的是一件好事。虽然考虑将其视为2-范畴（即使是...），但我认为这可能是不必要的。 - sclv

@sclv：在我看来，许多范畴论在Haskell中默认变得混乱，因为多态性和普遍的高阶函数意味着几乎任何类似于态射的东西都可以（并且必须）被压缩成Hask中的参数化态射。比较一下“为什么只有一些箭头在余单子和单子之间被反转？” - C. A. McCann

Answer 3

粗略地讲，Haskell使用一个类别进行范畴论，其对象是Haskell类型，箭头是这些类型之间的函数。它绝对不是用于建模范畴论的通用语言。

（数学上的）函子是一种将一个类别中的事物转化为另一个可能完全不同的类别中的事物的运算符。而自函子则是一种在相同源和目标类别上的函子。在Haskell中，函子是一种将Haskell类型范畴中的事物转化为该范畴中的其他事物的运算符，因此它总是一个自函子。

（如果您正在跟踪数学文献，则技术上，“（a->b）->（m a->m b）”操作只是自函子m的箭头部分，“m”是对象部分。）

当Haskellers谈论“在单子中工作”时，他们实际上是指在单子的Kleisli类别中工作。单子的Kleisli类别起初非常令人困惑，并且通常需要至少两种颜色的墨水来进行充分的解释，因此请以以下尝试为基础，并查阅一些参考资料（遗憾的是，Wikipedia在这里除了直接定义外毫无用处）。

假设您在Haskell类型类别C上有一个单子“m”。它的Kleisli类别Kl（m）与C具有相同的对象，即Haskell类型，但是Kl（m）中的箭头a~(f)~>b是C中的箭头a-(f)->mb。（我在我的Kleisli箭头中使用了波浪线来区分两个箭头）。请再次强调：Kl（C）的对象和箭头也是C的对象和箭头，但箭头指向Kl（C）中的不同对象而不是C中的对象。如果这不让您感到奇怪，请仔细再读一遍。

具体来说，考虑Maybe单子。它的Kleisli类别只是Haskell类型的集合，其箭头a~(f)~>b是函数a-(f)->Maybe b。或者考虑（State s）单子，其箭头a~(f)~>b是函数a-(f)->（State s b）== a-(f)->（s->（s，b））。无论哪种情况，您始终将波浪箭头写成简写形式，以对目标域的类型执行某些操作。

（请注意，State不是单子，因为State的种类为* -> * -> *，因此您需要提供其中一个类型参数以将其转换为数学单子。）

到目前为止，一切顺利，希望如此，但假设您要组合箭头a~(f)~>b和b~(g)~>c。这实际上是Haskell函数a-(f)->mb和b-(g)->mc，您无法组合它们，因为类型不匹配。数学解决方案是使用单子的“乘法”自然变换u:mm->m，如下所示：a~(f)~>b~(g)~>c == a-(f)->mb-(mg)->mmc-(u_c)->mc，以获得一个a->mc的箭头，它是所需的Kleisli箭头a~(f;g)~>c。

也许这里的一个具体例子有所帮助。在Maybe单子中，您无法直接组合函数f：a->Maybe b和g：b->Maybe c，但通过将g提升至

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

并且使用“显而易见”的方法

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

你可以形成组合 u . Maybe_g . f，这是您想要的函数a -> Maybe c。

在(State s) monad中，它类似但比较杂乱：给定两个单子函数 a ~(f)~> b 和 b ~(g)~> c，它们实际上是在内部进行了适当的转换成 a -(f)-> (s->(s,b)) 和 b -(g)-> (s->(s,c))，您可以将它们组合起来通过将 g 提升（lift）到

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

然后您将应用“乘法”自然变换u，即

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

这个函数有点像把 f 的最终状态插入到 g 的初始状态中。

Haskell 中，这种方式有些不自然，因此有 (>>=) 函数，它基本上与 u 做的事情相同，但更容易实现和使用。重要的是: (>>=) 不是自然变换 'u'。你可以用一个定义来表示另一个，所以它们是等价的，但它们不是同一件事。 Haskell 版本的 'u' 被写成 join。

Kleisli 类别定义中还缺少每个对象的恒等性：一个 ~(1_a)~> a，它其实是一个 -(n_a)-> ma，其中 n 是“单位”自然变换。在 Haskell 中，这被写作 return，并且似乎不会引起太多混淆。

在我学习 Haskell 之前，我学过范畴论，我也遇到了数学家所说的单子与在 Haskell 中的样子之间的不匹配问题。从另一个方向来看，这也并不容易！

- Dave Turner

---

谢谢，这非常有趣，尽管如你所说，Kleisli范畴似乎很令人困惑。我认为我从这个和其他解释中得到了一个共同的主题，它们似乎都是双层的。由于在此评论中没有足够的空间，我已经添加了自己的“答案”来尝试解释我的意思。 - Martin

Answer 4

我不确定我理解了问题，但是没错，Haskell中的monad被定义为三元组:

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

但是范畴论中的常见定义是另一个三元组：

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

有点混乱，但证明这两个定义相等并不难。 为了做到这一点，我们需要用(>>=)（反之亦然）来定义join。 第一步：

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

这使我们得到了x :: m (m a)。对于类型为m _的东西，我们能做的只有将(>>=)应用于它：

(x >>=) :: (m a -> m b) -> m b

现在我们需要一个作为(>>=)的第二个参数，而且，从我们拥有的连接类型中，我们有约束条件(x >>= y) :: ma。
所以这里的y将具有类型y :: ma -> ma，而id :: a -> a非常适合它：

join x = x >>= id

另一种方法

(>>=) :: ma -> (a -> mb) -> m b
(>>=) x y = ?

当 x :: m a 和 y :: a -> m b 时，想要从 x 和 y 获取 m b，我们需要一个类型为 a 的东西。
不幸的是，我们无法从 m a 中提取出 a。但是我们可以用其他东西来替代它（记住，单子也是一个函子）：

fmap :: (a -> b) -> m a -> m b
fmap y x :: m (m b)

它完美地适用于join的参数：(>>=) x y = join (fmap y x)。

- max taldykin

Answer 5

最好理解单子和计算效应的方法是从Haskell得到单子用于计算效应的概念，然后再看Haskell。特别是要看这篇论文：Notions of Computation and Monads，作者是E. Moggi。

此外，还可以看Moggi早期的一篇论文，其中展示了单子如何仅适用于lambda演算：http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.2787 单子捕获替换等内容（http://blog.sigfpe.com/2009/12/where-do-monads-come-from.html），而替换是lambda演算的关键，这就是为什么单子具有如此多的表达能力的一个很好的线索。

- sclv

Answer 6

从一种角度来看，IO可以被视为一种奇怪的状态单子。请记住，状态单子的形式如下：

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

在这里，“s”参数是您希望在计算中传递的数据类型。此版本的“State”没有“get”和“put”操作，我们不导出构造函数。

现在想象一种类型。

data RealWorld = RealWorld ......

这没有确切的定义，但是可以概括地说，类型为RealWorld的值持有计算机外整个宇宙的状态。当然，我们永远无法获得类型为RealWorld的值，但你可以想象一些类似的东西：

getChar :: RealWorld -> (RealWorld, Char)

换句话说，“getChar”函数获取键盘按下之前的宇宙状态，并返回按下的键以及按键后的宇宙状态。当然，问题在于之前的世界状态仍然可以被引用，在现实中是不可能的。

但现在我们这样写：

类型 IO = 状态RealWorld

getChar :: IO Char 从概念上讲，我们所做的只是将以前版本的“getChar”包装为状态操作。但通过这样做，我们不能再访问“RealWorld”值，因为它们被包裹在State单子里面。

因此，当Haskell程序想要更换灯泡时，它会拿起灯泡并在IO内部应用“rotate”函数来改变RealWorld的值。

- Paul Johnson

---

请注意，解释Haskell的IO的State RealWorld的想法是一个持久的谬论。您可以在此SO评论中找到一些解释。该模型仅适用于纯顺序、非交互式的命令式计算，并且在交互性和并发性方面会出现问题。（并发是关键所在，而交互性是并发的一个特例，尽管通常不被视为这样。） - Conal

我并不认为这是一个大问题。从程序（虽然有点自恋）的角度来看，“RealWorld”对象是一个黑匣子；它既不知道也不关心里面发生了什么。上面的模型中没有描述时间的内容，因此从程序的角度来看，“getChar”只是一个RealWorld的函数。当然，一旦您尝试两次访问同一个RealWorld时，这个模型就会崩溃，但正如我所说的，这就是我们将其放入State monad中的原因。 - Paul Johnson

Answer 7

尽管单子最初来自于范畴论，但这并不意味着范畴论是你能够观察它们的唯一抽象上下文。另一个视角是由 操作语义 给出的。想了解更多，请查看我的操作单子教程。

- Heinrich Apfelmus

Answer 8

到目前为止，我认为将范畴论中的单子(monads)和Haskell中的单子联系起来的最接近的解释是，单子是一个单子(monoid)，其对象的类型为a->m b。我可以看出这些对象非常接近于一个自函子(endofunctor)，因此这些函数的组合与程序语句的命令序列相关联。同时，返回IO函数的函数在纯函数式代码中也是有效的，直到从外部调用内部函数。

这个id元素是'a -> m a'，非常契合，但乘法元素是函数组合，应该是：

(>>=) :: Monad m => m a -> (a -> m b) -> m b

这不完全是函数组合，但足够接近了（我认为要想得到真正的函数组合，我们需要一个互补函数，将m b转换回a，然后如果我们成对应用它们，就能得到函数组合？），我不太确定如何从这里得到这个：

(>>=) :: Monad m => m a -> (a -> m b) -> m b

我有一种感觉，在我读过的所有东西中，可能已经看到了对此的解释，但第一次阅读时并没有理解其意义，因此我将重新阅读以尝试找到其解释。

另一件我想做的事情是将所有不同的范畴论解释联系在一起：自函子+2个自然变换，Kleisli范畴，对象为单子的单子等等。对我来说，似乎将所有这些解释联系起来的事情是它们都是两级的。也就是说，通常我们将范畴对象视为黑盒子，在外部交互中暗示其属性，但在这里似乎需要进入对象的内部一层，以查看发生了什么？我们可以解释单子而不需要这样做，但只有在接受明显任意的构造时才能这样做。

马丁

- Martin

---

不确定您所说的“两级”是什么意思：单子与其Kleisli类别之间的关系并不比我早些时候的回复更深入。要通过真正的函数组合来实现（>=>），您只需将第二个参数liftM，组合并join输出即可。实现(>>=)也是相同的：将第二个参数liftM，应用于第一个参数，并将join应用于输出。liftM只是应用了自函子，而join则是单子乘法。您能详细说明一下“进入对象”的含义吗？因为这对以上任何内容都不必要（并且是反范畴论的）。 - Dave Turner

也许我误解了？我认为第一层是类别C，Kleisli类别以及它们之间的映射（箭头），因此类别C和Kleisli类别内部的对象和箭头将构成第二层。 - Martin

哦，我明白了。你说得对，但我不知道第二层是否能让你更深入地了解Haskell。如果你想变得高端一些，Kleisli范畴是特殊的，因为它（与C的关系）是在“给你最初想到的单子”的东西类别中的一个初始对象，这是比你的“第一”层更高的层次，但这个事实绝对不能告诉你任何有用的关于Haskell的信息。对我来说，理解单子数学的关键是理解C和Kl(m)之间的关系。我很震惊维基教科书页面上甚至没有提到Kleisli这个词！ - Dave Turner

Answer 9

请看这个问题：链接到“chaining operations the only thing that the monad class solves?”

在这个问题中，我解释了我们必须区分Monad类和解决单个问题的各个类型之间的区别。Monad类本身仅解决“使用选择链接操作”的重要问题，并通过“继承”使其可用于作为其实例的类型。

另一方面，如果一个给定的解决特定问题的类型面临“使用选择链接操作”的问题，则应将其作为Monad类的实例（继承）。

事实上，并不是所有问题都可以通过成为Monad来解决。这就像说“轮子”可以解决许多问题，但实际上“轮子”只能解决一个问题，而带有轮子的东西可以解决许多不同的问题。

- cibercitizen1