haskell - Monad 理论和 Haskell

Question

大多数教程似乎都给出了很多 monad 的例子(IO、状态、列表等)，然后期望读者能够抽象出总体原理，然后再提到范畴论。我不倾向于通过尝试从示例中进行概括来很好地学习，我想从理论的角度理解为什么这种模式如此重要。

从这个线程来看:
Can anyone explain Monads?
这是一个常见问题，我已经尝试查看建议的大多数教程(除了无法在我的 linux 机器上播放的 Brian Beck 视频):

有谁知道从类别理论开始并用这些术语解释 IO、状态、列表单子(monad)的教程？以下是我不成功的尝试:

据我了解，一个单子(monad)由一个三元组组成:一个内仿函数和两个自然变换。

仿函数通常显示为以下类型:
(a -> b) -> (m a -> m b)
我包括第二个括号只是为了强调对称性。

但是，这是一个内仿函数，所以域和共域不应该像这样吗？:

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

我认为答案是 domain 和 codomain 都具有以下类型:

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

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

当我们继续进行自然转变时，情况会变得更糟。如果我理解正确，自然变换是二阶仿函数(具有某些规则)，它是从一个仿函数到另一个仿函数的仿函数。因此，既然我们已经在上面定义了仿函数，自然变换的一般类型将是:
((a -> b) -> (m a -> m b)) -> ((a -> b) -> (m a -> m b))

但我们使用的实际自然变换有以下类型:

一个 -> 米一个

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

这些是上述一般形式的子集吗？为什么它们是自然转变？

马丁

Answer 1

一个快速的免责声明:总的来说，我对类别理论有点动摇，但我觉得你至少对它有些熟悉。希望我不会对此做太多的散列......

Does anyone know of a tutorial that starts from category theory and explains IO, state, list monads in those terms?

首先忽略IO现在，它充满了黑暗魔法。出于与 State 相同的原因，它可以用作命令式计算的模型。适用于有状态计算的建模，但与后者不同IO是一个黑匣子，无法从外部推断出一元结构。

The functor is usually shown with the type: (a -> b) -> (m a -> m b) I included the second bracket just to emphasise the symmetry.

But, this is an endofunctor, so shouldn't the domain and codomain be the same like this?:

我怀疑您误解了 Haskell 中的类型变量与类别理论概念的关系。

首先，是的，它在 Haskell 类型的类别上指定了一个 endofunctor。类型变量，例如 a然而，它不属于这一类；它是一个在类别中的所有对象上(隐式地)普遍量化的变量。因此，类型 (a -> b) -> (a -> b)仅描述将每个对象映射到自身的内仿函数。

类型构造函数描述了对象上的单射函数，其中构造函数的 codomain 的元素除了作为类型构造函数的应用程序之外不能以任何方式描述。即使两个类型构造函数产生同构的结果，结果类型仍然是不同的。请注意，在一般情况下，类型构造函数不是仿函数。

类型变量m那么，在仿函数签名中，代表一个单参数类型构造函数。断章取义，这通常会被解读为通用量化，但在这种情况下这是不正确的，因为不存在这样的函数。相反，类型类定义绑定(bind) m并允许为特定类型的构造函数定义此类函数。

然后，生成的函数表示对于任何类型的构造函数 m其中有 fmap为任意两个对象定义 a和 b以及它们之间的态射，我们可以通过应用 m 找到给定类型之间的态射至a和 b .

请注意，虽然上面确实在 上定义了一个内仿函数。哈斯克 ，它甚至不足以描述所有这些内仿函数。

But the actual natural transformations we are using have type:

a -> m a

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

Are these subsets of the general form above? and why are they natural transformations?

嗯，不，他们不是。自然转换大致是仿函数之间的函数(不是仿函数)。指定单子(monad) M 的两个自然变换看起来像 I -> M其中 I 是恒等仿函数，M ∘ M -> M在哪里 ∘是仿函数组合。在 Haskell 中，我们没有直接使用真身份仿函数或仿函数组合的好方法。相反，我们丢弃了恒等仿函数，只得到 (Functor m) => a -> m a首先，将嵌套类型构造函数应用程序写为 (Functor m) => m (m a) -> m a第二个。

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

就特定的单子(monad)而言，如果您想要更数学的描述，这里有一个示例的速写:

对于某些固定类型 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 .这些类型建议非curried函数应用和元组构造；随时验证这些是否按预期工作。

一个附加函数通过仿函数的组合产生一个单子(monad)，所以取 G ∘ F 并扩展定义，我们得到 G (F x) = S -> (S, x)，这是 State 的定义单子(monad)。 unit因为附件当然是return ;你应该可以使用counit定义 join .