21

好吧，我正在研究 Haskell Monads。当我阅读维基百科分类理论文章时，我发现单子态射的签名看起来很像逻辑中的重言式，但你需要转换M a为~~A，这里~是逻辑否定。

return :: a -> M a -- Map to tautology A => ~~A, double negation introduction
(>>=) :: M a -> (a -> M b) -> M b -- Map to tautology ~~A => (A => ~~B) => ~~B

其他操作也是重言式：

fmap :: (a -> b) -> M a -> M b -- Map to (A => B) -> (~~A => ~~B)
join :: M (M a) -> M a -- Map to ~~(~~A) => ~~A

也可以理解为，根据普通函数式语言的Curry-Howard对应是直觉逻辑，而不是经典逻辑，所以不能指望像重言式一样~~A => A可以有对应。

但我在想别的东西。为什么单子只能与双重否定有关？单一否定的对应关系是什么？这使我得到以下类定义：

class Nomad n where
    rfmap :: (a -> b) -> n b -> n a
    dneg :: a -> n (n a)

return :: Nomad n => a -> n (n a)
return = dneg
(>>=) :: Nomad n => n (n a) -> (a -> n (n b)) -> n (n b)
x >>= f = rfmap dneg $ rfmap (rfmap f) x

这里我定义了一个叫做“Nomad”的概念，它支持两种操作（都与直觉逻辑中的一个逻辑公理有关）。请注意，“rfmap”这个名称意味着它的签名类似于 functor 的fmap，但结果中a和的顺序b相反。现在我可以用它们重新定义 Monad 操作，用 replace M ato n (n a)。

那么现在让我们进入问题部分。Monad是范畴论的一个概念，这似乎意味着我的“Nomad”也是一个范畴论的概念。那是什么？有用吗？该课题是否有论文或研究成果？

4

2 回答 2

20

双重否定是一个特殊的单子

data Void --no constructor because it is uninhabited

newtype DN a = DN {runDN :: (a -> Void) -> Void}

instance Monad DN where
   return x = DN $ \f -> f x
   m >>= k  = DN $ \c -> runDN m (\a -> runDN (k a) c))

实际上，这是一个更一般的单子的例子

type DN = Cont Void
newtype Cont r a = Cont {runCont :: (a -> r) -> r}

这是继续传递的单子。

像“monad”这样的概念不仅由签名定义，还由一些法律定义。所以，这里有一个问题，你的建筑的法律应该是什么？

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

是范畴论中众所周知的一种方法的签名，即逆变函子。它基本上遵循与函子相同的定律（保留（共）组成和同一性）。实际上，逆变函子正是相反范畴的函子。由于我们对应该是内函子的“haskell 函子”感兴趣，我们可以看到“haskell 逆变函子”是函子Hask -> Hask_Op。

另一方面，怎么办

a -> f (f a)

这应该有什么法律？我有一个建议。在范畴论中，可以在 Functor 之间进行映射。F, G给定两个从类别C到类别的函子，从到D的自然变换是 中的态射FGD

forall a. F a -> G a

遵守某些相干定律。您可以使用自然变换做很多事情，包括使用它们来定义“函子类别”。但是，经典的笑话（由于 Mac Lane）是发明范畴来谈论函子，发明函子来谈论自然变换，发明自然变换来谈论附属词。

如果存在两个自然变换，则函子F : D -> C和函子G : C -> D形成从C到的附属物D

unit : Id -> G . F
counit : F . G -> Id

这种附加的想法是理解单子的常用方法。每个附加词都以一种完全自然的方式产生一个单子。也就是说，由于这两个函子的组合是一个内函子，并且你有类似于返回的东西（单元），你所需要的只是连接。但这很容易，join 只是一个功能G . F . G . F -> G . F，您只需在“中间”使用 counit 即可。

那么，有了这一切，你在寻找什么？好

dneg :: a -> n (n a)

看起来与unit逆变函子与自身的附属物完全一样。因此，您的Nomad类型很可能（当然，如果您使用它来构造 monad 是正确的）与“自伴随的逆变函子”完全相同。搜索自伴随函子将带您回到双重否定和连续传递……这正是我们开始的地方！

编辑：几乎可以肯定上面的一些箭头是向后的。不过，基本的想法是正确的。您可以使用以下引文自己解决：

关于范畴论的最好的书可能是，

  • Steve Awodey，范畴论
  • Sanders Mac Lane，工作数学家的分类

尽管存在许多更平易近人的介绍性书籍，包括 Benjamin Pierces 为计算机科学家编写的关于范畴论的书。

在线视频讲座

许多论文探讨了延续单子的附加角，例如

  • Hayo Thielecke，连续语义和自伴随

搜索词“self adjoint”、“continuation”和“monad”都很好。此外，许多博主也写过关于这些问题的文章。如果你用谷歌搜索“monads 来自哪里”，你会得到有用的结果，比如来自 n 类别咖啡馆的这个，或者来自sigfpe 的这个。还有 Sjoerd Vissche与 Comonad 阅读器 的链接。

于 2012-12-20T13:32:24.020 回答
8

那将是一个自伴逆变函子。rfmap提供逆变函子部分，dneg是附加的单位和单位。

Op r是一个例子，它创建了延续单子。有关某些代码，请参阅http://hackage.haskell.org/package/adjunctions中的逆变模块。

您应该阅读http://comonad.com/reader/2011/monads-from-comonads/，这是相关且非常有趣的。

于 2012-12-20T12:29:08.087 回答