好吧,我正在研究 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”也是一个范畴论的概念。那是什么?有用吗?该课题是否有论文或研究成果?
最佳答案
双重否定是一个特殊的单子(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 是正确的)与“自伴的逆变仿函数”完全相同。搜索自伴随仿函数将带您回到双重否定和连续传递……这正是我们开始的地方!编辑:几乎可以肯定上面的一些箭头是向后的。不过,基本的想法是正确的。您可以使用以下引文自己解决:
关于范畴论的最好的书可能是,
尽管存在许多更平易近人的介绍性书籍,包括 Benjamin Pierces 为计算机科学家编写的关于类别理论的书籍。
在线视频讲座
许多论文探讨了延续单子(monad)的附加角,例如
搜索词“self adjoint”、“continuation”和“monad”都很好。此外,许多博主也写过关于这些问题的文章。如果你用谷歌搜索“monads 来自哪里”,你会得到有用的结果,例如 this one来自 n 类咖啡馆,或 this one来自 sigfpe。还有 Sjoerd Vissche 的 link给 Comonad 读者。
关于haskell - 有什么叫 "semi-monad"或 "counter-monad"吗?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/13971711/