Ear*_*ine 20 monads haskell category-theory
好吧,我正在研究Haskell Monads.当我阅读Wikibook 类别理论文章时,我发现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"也是一个范畴理论概念.那是什么？它有用吗？这个主题是否有任何论文或研究成果？
Phi*_* JF 19
双重否定是一个特殊的单子
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"这样的概念不是仅仅通过签名来定义,而是通过某些定律来定义.所以,这是一个问题,你的建筑法律应该是什么？
(a -> b) -> f b -> f a
是类别理论众所周知的方法的签名,即逆变函子.它遵循与仿函数基本相同的规律(保留(共同)构成和身份).实际上,逆变函子恰好是对立类的一个算符.由于我们对应该是endo-functors的"haskell仿函数"感兴趣,我们可以看到"haskell逆变仿函数"是一个仿函数Hask -> Hask_Op.
另一方面,怎么样
a -> f (f a)
这有什么法律规定？我有个建议.在类别理论中,可以在Functors之间进行映射.鉴于从两个函子F, G分别从类别C到类别D,一个自然的转变,从F以G处于射D
forall a. F a -> G a
遵守某些连贯性法律.您可以使用自然变换做很多事情,包括使用它们来定义"仿函数类别".但是,经典的笑话(由于Mac Lane)是因为发明类别是为了讨论仿函数,发明仿函数是为了谈论自然变换,而发明了自然变换来讨论关联.
如果存在两个自然变换,则仿函数F : D -> C和仿函数G : C -> D形成一个附属物CD
unit : Id -> G . F
counit : F . G -> Id
这种附属概念是理解单子的常用方法.每个附属物都以完全自然的方式产生一个单子.也就是说,由于这两个仿函数的组合是一个endofunctor,并且你有类似返回(单位)的东西,你只需要连接.但这很容易,加入只是一个功能G . F . G . F -> G . F,你只需使用"在中间"的国家.
那么,有了这一切,你在寻找什么？好
dneg :: a -> n (n a)
看起来unit与逆变函子的自身结合完全一样.因此,你的Nomad类型很可能(当然如果你使用它来构造一个monad是正确的)与"一个自相伴的逆变函子"完全相同.搜索自伴函子会让你回到Double-negation和Continuation传递......这就是我们开始的地方!
编辑:几乎可以肯定,上面的一些箭头是倒退的.不过,基本的想法是正确的.您可以使用下面的引文自行解决:
关于范畴理论的最佳书籍可能是,
虽然存在许多更平易近人的介绍书,包括本杰明皮尔斯的计算机科学家类别理论书.
在线视频讲座
例如,许多论文探讨了连续monad的附加角度
搜索词"self adjoint","continuation"和"monad"都很好.此外,一些博客撰写了关于这些问题的文章.如果谷歌"里做的单子来自"你得到有用的结果,这一次从n类咖啡馆,或者这一个从SIGFPE.Sjoerd Vissche 也是Comonad读者的链接.
这将是一个自伴的逆变函子.rfmap提供逆变函子部分,并且dneg是附属的单位和对象.
Op r是一个例子,它创建了continuation monad.有关一些代码,请参阅http://hackage.haskell.org/package/adjunctions中的逆变量模块.
你应该阅读http://comonad.com/reader/2011/monads-from-comonads/,这是相关的,非常有趣.