haskell - 有什么叫 "semi-monad"或 "counter-monad"吗？

Question

好吧，我正在研究 Haskell Monads。当我阅读维基百科 Category theory文章，我发现monad态射的签名在逻辑上看起来很像重言式，但是你需要转换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 这样的重言式可以有对应关系。

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

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”意味着它的签名类似于仿函数的 fmap。 , 但 a 的顺序和 b结果相反。现在我可以用它们重新定义 Monad 操作，替换 M a至 n (n a) .

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

Answer 1

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

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))

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

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

这是继续传递的单子(monad)。

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

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

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

另一方面，怎么办

a -> f (f a)

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

forall a. F a -> G a

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

一个仿函数 F : D -> C和一个仿函数 G : C -> D从 C 形成一个附属词至 D如果存在两个自然变换

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

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

那么，有了这一切，你在寻找什么？出色地

dneg :: a -> n (n a)

看起来完全像 unit逆变仿函数与自身的附加。因此，您的 Nomad type 很可能(当然，如果您使用它来构造 monad 是正确的)与“自伴的逆变仿函数”完全相同。搜索自伴随仿函数将带您回到双重否定和连续传递……这正是我们开始的地方!

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

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

Steve Awodey，类别理论

Sanders Mac Lane，工作数学家分类

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

在线视频讲座

来自 Oregon Programming Language Summer School 的 Steve Awodey 的范畴理论讲座

Catsters 在 youtube 上的简短讲座，indexed here ，请特别注意关于附件的视频

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

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

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