有没有叫做“半单子”或“计数器单子”的东西？

Question

好的，我正在学习 Haskell 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对应（Curry-Howard correspondence），它是直觉逻辑而不是古典逻辑，因此我们不能期望像~~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”也是一个范畴论概念。那么它是什么？它有用吗？这个主题是否存在任何论文或研究结果？

- Earth Engine

---

rfmap 是针对逆变函子的一种操作。 - shachaf

您的问题标题询问是否存在“半单子”，但实际上您的问题方向不同。为了完整起见，应该指出，“半单子”可能是指没有单元操作的单子（即在Haskell中没有明确定义的'return :: a -> m a'），或者其单元操作不像单元那样行为良好，例如，‘(return x) >>= f = / = f x’。这类似于半群的概念，它是一个没有单位（或表现良好的单位）的幺半群。 - dorchard

当我说“半单子”是指“Nomad”看起来像“Monad”的一半，因为“n(n a)”是一个明确定义的“Monad”。 - Earth Engine

Answer 1

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

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}

这是延续传递的单子。

像“单子”这样的概念不仅由签名定义，还有一些规则。所以，这里有一个问题，你的构造应该遵守哪些规则？

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

方法的签名在范畴论中被称为逆变函子，它与普通函子遵循基本相同的规律（保留（共）合成和恒等性）。事实上，逆变函子恰好是一个映射到对偶范畴的函子。由于我们感兴趣的是“Haskell 函子”，这些函子应该是自函子，我们可以将 “Haskell 逆变函子” 视为一个从 Hask -> Hask_Op 的函子。

另一方面，有关什么？

a -> f (f a)

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

forall a. F a -> G a

这里所说的自然变换是遵循一定连贯规律的一类函数。利用自然变换，您可以做很多事情，包括使用它们来定义“函子范畴”。但是，经典笑话（由Mac Lane创造）是类别的发明是为了谈论函子，函子的发明是为了谈论自然变换，而自然变换的发明是为了谈论伴随。

如果存在两个自然变换，那么从C到D的函子F：D -> C和从C到D的函子G：C -> D会形成一个从C到D的伴随。

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

这个所谓的伴随是理解单子的常用方式。每个伴随都自然地导出一个单子。也就是说，由于这两个函子的组合是一个自身函子，你会有类似于return（单位元素）的东西，你所需要的只是join。但那很容易，join 只是一个函数 G . F . G . F -> G . F，你可以通过使用“中间”的余单元来得到。

那么，有了所有这些，你在寻找什么呢？嗯

dneg :: a -> n (n a)

看起来和反变函子自身的伴随的“单位”完全相同。 因此，如果您使用它构建一个单子正确，则Nomad类型很可能（肯定）与“自共轭的反变函子”完全相同。 搜索自共轭的函子将使您回到双重否定和延续传递......这正是我们开始的地方！

---

编辑：上面的箭头几乎可以确定有一些错误。 不过基本思想是正确的。 您可以使用下面的引用自行解决：

范畴论最好的书籍可能是：

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

虽然还有很多更易于理解的介绍性书籍，包括Benjamin Pierce撰写的面向计算机科学家的类别论书籍。

在线视频讲座

• Steve Awodey在 Oregon Programming Language Summer School 中提供的《范畴论》讲座
• Catsters在Youtube上的短讲，在此索引，特别关注其关于伴随的视频

许多论文探讨了延续单子中的伴随角度，例如：

• Hayo Thielecke，《延续语义和自共轭性》

搜索词“自共轭”、“延续”和“单子”是不错的选择。 此外，许多博客也写过这些问题。 如果您搜索“单子来自哪里”，则会得到有用的结果，例如从n范畴咖啡厅的这篇文章，或者来自sigfpe的这篇文章。 另请参阅Sjoerd Vissche's的链接到Comonad reader。

- Philip JF

---

dneg也是余单位（箭头翻转，因为余单位的组成部分在Hask^op中是箭头）。而用于构成伴随对的自然同构homC(F–,–) → homD(–,G–)的恒等式，是因为hom_(Hask^op)(a,b) = hom_Hask(b,a)。因此，一个Nomad就是“一个自反的协变函子”。 - Sjoerd Visscher

很好的回答。您能否在文本中添加一些参考资料或建议一些进一步阅读的来源？我想将其标记为答案。 - Earth Engine

抱歉打扰了一个旧的帖子，但是当你说“协变”时，你是指“逆变”吗？ - Jonathan Sterling

@JonathanSterling 可能吧。我想现在已经修复了。我完全不记得写过这个，所以再次看到它很有趣。 - Philip JF

Answer 2

那将是一个自伴逆变函子。rfmap提供了逆变函子部分，而dneg是配准的单位和余单位。

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

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

- Sjoerd Visscher