Monads作为附件

我一直在阅读有关monad的分类理论。 单子的一个定义使用一对伴随函数。 单子是通过使用这些函数的往返来定义的。 显然附加类在分类理论中是非常重要的,但是我还没有看到Haskell monads在伴随函数方面的任何解释。 有没有人给它一个想法?

编辑 :只是为了好玩,我打算这样做的权利。 原始答案保存在下面

目前的category-extras的附加代码在附件包中: http : //hackage.haskell.org/package/adjunctions

我只是明确而简单地通过状态monad。 此代码使用来自变换器包的Data.Functor.Compose ,但是是其他自包含的。

f(D→C)和g(C→D)之间的一个连接点写成f – | 克,可以用多种方式来表征。 我们将使用counte / unit(epsilon / eta)描述,它给出了两个自然变换(仿函数之间的态射)。

 class (Functor f, Functor g) => Adjoint fg where counit :: f (ga) -> a unit :: a -> g (fa) 

请注意,议会中的“a”实际上是C中的身份函子,单位中的“a”实际上是D中的身份函子。

我们也可以从counte / unit定义中恢复hom-set的附属定义。

 phiLeft :: Adjoint fg => (fa -> b) -> (a -> gb) phiLeft f = fmap f . unit phiRight :: Adjoint fg => (a -> gb) -> (fa -> b) phiRight f = counit . fmap f 

无论如何,我们现在可以从我们的单位/议会联盟中定义一个Monad,如下所示:

 instance Adjoint fg => Monad (Compose gf) where return x = Compose $ unit x x >>= f = Compose . fmap counit . getCompose $ fmap (getCompose . f) x 

现在我们可以实现(a,)和(a – >)之间的经典关系:

 instance Adjoint ((,) a) ((->) a) where -- counit :: (a,a -> b) -> b counit (x, f) = fx -- unit :: b -> (a -> (a,b)) unit x = \y -> (y, x) 

现在是一个types的同义词

 type State s = Compose ((->) s) ((,) s) 

如果我们用ghci加载它,我们可以证实国家恰恰是我们经典的国家单子。 请注意,我们可以采取相反的组合,并得到Costate Comonad(又名商店comonad)。

还有一些其他的辅助手段(比如(Bool,Pair)),我们可以把它们变成单子,但它们却是一些奇怪的单子。 不幸的是,我们不能以愉快的方式直接在Haskell中引发Reader和Writer。 我们可以做Cont,但是正如copumpkin所描述的那样,它需要来自相反类别的一个连接,所以它实际上使用了“Adjoint”typestypes的一个不同的“forms”,它颠倒了一些箭头。 这种forms也在辅助包中的不同模块中实现。

Derek Elkins在“Monad Reader 13 – 用分类理论计算Monad”中的文章以不同的方式介绍了这种材料: http : //www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

另外,Hinze最近的Kan扩展程序优化论文从MonSet之间的连接中逐步构build了list monad: http : //www.cs.ox.ac.uk/ralf.hinze/Kan.pdf


老答案:

两个参考。

1)类别附加服务一如既往地提供辅助表示,以及如何从它们中产生monad。 像往常一样,这是很好的想法,但很轻的文档: http : //hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html

2)-Cafe也提供了一个有前途但简短的讨论副作用的讨论。 其中一些可能有助于解释类别附加说明: http : //www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html

德里克·艾尔金斯(Derek Elkins)最近在晚餐中向我展示了如何通过组合(_ -> k)逆变函数与自身的联系,因为它碰巧是自伴的。 这就是你从(a -> k) -> k中得到的。 然而,它的议会导致双重否定消除,这在Haskell中是不能写的。

对于一些Agda代码来说明和certificate这一点,请参阅http://hpaste.org/68257

这是一个古老的线索,但我觉得这个问题很有趣,所以我自己做了一些计算。 希望巴托斯仍然在那里,可能会读这..

事实上,艾伦贝格 – 摩尔build筑在这种情况下确实给出了一个非常清晰的图景。 (我将用类似于Haskell的CWM符号语法)

T是单子< T,eta,mu >eta = returnmu = concat ),并考虑T代数h:T a -> a

(请注意, T a = [a]是一个自由幺半群<[a],[],(++)> ,即identity []和multiplication (++)

根据定义, h必须满足hT h == h.mu ah.eta a== id

现在,一些简单的图表certificate了h实际上是在一个(由x*y = h[x,y]定义的)上诱导出一个monoid结构,并且h成为这个结构的幺半群同态。

相反,在Haskell中定义的任何幺半群结构< a,a0,* >自然被定义为一个T-代数。

以这种方式( h = foldr ( * ) a0 ,一个用(*)替代(:)的函数,以及将[]映射到a0的函数)。

因此,在这种情况下,T代数的范畴就是Haskell,HaskMon中定义的幺半群结构范畴。

(请检查T代数中的态射实际上是幺半群同态。)

它还将HaskMon中的列表表示为通用对象,就像Grp中的免费产品,CRng中的多项式环等一样。

对应于上述结构的辅助是< F,G,eta,epsilon >

哪里

  • F:Hask -> HaskMon ,它对a生成的自由monoid采用typesa,即[a]
  • G:HaskMon -> Hask ,健忘函数(忘记乘法),
  • eta:1 -> GF ,由\x::a -> [x]定义的自然转换,
  • epsilon: FG -> 1 ,由上面折叠函数定义的自然变换(从一个自由幺半群到其商幺半群的“正则投射”),

接下来,还有另一个“Kleisli类别”和相应的附件。 你可以检查它是否是types为a -> T b的Haskelltypes,其组成由所谓的“Kleisli组合” (>=>) 。 一个典型的Haskell程序员会发现这个类更熟悉。

最后,如CWM所示,T代数(Kleisli类别)的类别在适当的意义上成为定义列表单子T的类别中的terminal(或初始)对象。

我build议为二叉树函子T a = L a | B (T a) (T a)做一个类似的计算 T a = L a | B (T a) (T a)检查你的理解。

我发现了Eilenberg-Moore的任何monad的附加函数的标准构造,但我不确定是否增加了对这个问题的洞察力。 第二类是T-algebras。 AT代数将“产品”添加到最初的类别。

那么对于monad列表来说它将如何工作呢? 列表monad中的函数由一个types构造函数组成,例如Int->[Int]和函数映射(例如,映射到列表的标准应用程序)。 代数添加了从列表到元素的映射。 一个例子是添加(或相乘)整数列表的所有元素。 函数F采用任何types,例如Int,并将其映射到在Int列表上定义的代数,其中产品由一元连接定义(反之亦然,连接定义为产品)。 健忘的函子G代数并忘记了产品。 然后使用伴随函数的FG对以通常的方式构造单子。

我必须说我不聪明。

如果你有兴趣,下面是关于Monad和辅助函数在编程语言中的作用的非专家的一些想法:

首先,对于给定的monad T ,存在对T的Kleisli范畴的唯一连接。 在Haskell中,monads的使用主要局限于这一类的操作(这本质上是一个自由代数的范畴,没有商)。 实际上,Haskell Monad所做的一切都是通过使用doexpression式(>>=)等组成一些types为a->T b Kleisli态射来创build一个新的态射。 在这种情况下,monad的作用仅限于记号的经济性。一种利用态射的联想性能够写(比如说) [0,1,2]而不是(Cons 0 (Cons 1 (Cons 2 Nil))) ,也就是说,你可以写序列而不是树。

即使使用IO monads也不是必需的,因为现在的Haskelltypes系统足够强大,可以实现数据封装(存在types)。

这是我对你原来的问题的回答,但是我很好奇Haskell的专家对此有何评论。

另一方面,正如我们已经注意到的,单子和(T)代数的附加之间也有1-1对应关系。 在MacLane的术语中,伴随是“expression类别的等价方法”。 在一个典型的辅助设置中, F是一个“自由代数生成器”,G是一个“健忘函子”,相应的monad将(通过使用T代数)描述(以及何时)在X的对象上构造A的代数结构。

在Hask和单子T的情况下, T引入的结构是monoid的结构,这可以通过单子的理论提供的代数方法来帮助我们build立代码的性质(包括正确性)。 例如,只要<a,(*),e>是一个monoid,函数foldr (*) e::[a]->a就可以很容易地被看作是一个关联操作,这个事实可以被编译器来优化计算(例如通过并行)。 另一个应用是使用分类方法在函数式编程中识别和分类“recursion模式”,希望(部分地)处理“函数式编程的转向”Y(任意recursion组合)。

显然,这种应用是类别理论(MacLane,Eilenberg等)创造者的主要动机之一,即build立类别的自然等价性,并将一个着名的方法转化为另一个类别(例如拓扑空间的同调方法,编程的代数方法等)。 在这里,伴随物和单体是利用这些类别连接的不可或缺的工具。 (顺便说一下,单子(及其双子,共同子)的概念是如此笼统,以至于甚至可以定义哈斯克尔types的“同调”。但我还没有给出一个想法。)

至于你提到的非决定性的function,我还有很多话要说…但是请注意, 如果某个类别A <F,G>:Hask->A定义了列表单元T ,则必须有一个唯一的“比较函子” K:A->MonHask (Haskell中可定义的单K:A->MonHask类别) 。 实际上,这意味着您的兴趣类别必须是某种受限forms的monoids类别(例如,它可能缺less一些商数,而不是自由代数)以便定义列表monad。

最后,有一些评论:

我在上T a1 .. an = T1 T11 .. T1m | ...文章中提到的二叉树函子很容易推广到任意数据typesT a1 .. an = T1 T11 .. T1m | ... T a1 .. an = T1 T11 .. T1m | ... 也就是说,Haskell中的任何数据types自然都定义了monad(连同相应的代数类别和Kleisli类别),这只是Haskell中任何数据构造函数的总和。 这就是为什么我认为Haskell的Monad类不仅仅是语法糖(当然这在实践中非常重要)的另一个原因。