Mar*_*tin 35 theory monads haskell types
大多数教程似乎提供了很多monad(IO,状态,列表等)的例子,然后期望读者能够抽象出整体原则,然后他们提到类别理论.通过尝试从例子中进行概括,我不会学得很好,我想从理论的角度理解为什么这种模式如此重要.
从这个线索来看: 任何人都可以解释Monads吗？ 这是一个常见的问题,我已经尝试查看大多数建议的教程(除了我的linux机器上不能播放的Brian Beck视频):
有没有人知道从类别理论开始的教程,并用这些术语解释IO,状态,列表monad？以下是我未能成功的尝试:
据我所知,monad包含一个三元组:一个endo-functor和两个自然变换.
仿函数通常显示类型:(a - > b) - >(ma - > mb)我包括第二个括号只是为了强调对称性.
但是,这是一个endofunctor,所以域和codomain不应该像这样吗？:
(a - > b) - >(a - > b)
我认为答案是域和codomain都有一种类型:
(a - > b)| (ma - > mb)| (mma - > mmb)等......
但我不确定这是否有效或符合给定的仿函数的定义？
当我们继续进行自然变革时,它会变得更糟.如果我理解正确,自然变换是二阶函子(具有某些规则),它是从一个仿函数到另一个仿函数的仿函数.因为我们已经定义了上面的仿函数,一般类型的自然变换将是:((a - > b) - >(ma - > mb)) - >((a - > b) - >(ma - > mb ))
但是我们使用的实际自然变换有类型:
a - > ma
ma - >(a - > mb) - > mb
这些一般形式的子集是否在上面？为什么它们会自然变换？
马丁
C. *_*ann 18
一个快速的免责声明:我对类别理论总的来说有点不稳定,但我得到的印象是你至少对它有一些熟悉.希望我不会过多地讨论这个...
有没有人知道从类别理论开始的教程,并用这些术语解释IO,状态,列表monad？
首先,暂时忽略IO它,它充满了黑魔法.它作为命令式计算的模型起作用,其原因State与建模有状态计算相同,但与后者不同的IO是黑盒子,无法从外部推断出monadic结构.
仿函数通常显示类型:(a - > b) - >(ma - > mb)我包括第二个括号只是为了强调对称性.
但是,这是一个endofunctor,所以域和codomain不应该像这样吗？:
我怀疑你是否误解了Haskell中的类型变量与类别理论概念的关系.
首先,是的,它指定了一个关于Haskell类型的endofunctor.但是,类型变量a不属于此类别中的任何类型; 它是一个变量,它(隐式地)对该类别中的所有对象进行普遍量化.因此,该类型(a -> b) -> (a -> b)仅描述将每个对象映射到自身的endofunctors.
类型构造函数描述了对象的内射函数,其中构造函数的codomain的元素不能通过任何方式描述,除非作为类型构造函数的应用程序.即使两个类型构造函数产生同构结果,结果类型仍然是不同的.请注意,在一般情况下,类型构造函数不是函子.
m然后,仿函数签名中的类型变量表示单参数类型构造函数.在上下文中,这通常被理解为通用量化,但在这种情况下这是不正确的,因为不存在这样的函数.相反,类型类定义绑定m并允许为特定类型构造函数定义此类函数.
新的函数,然后说,对任何类型的构造m已fmap定义,对于任何两个物体a,并b和它们之间的态射,我们可以发现通过应用给出的类型之间的态射m来a和b.
请注意,虽然上面的内容确实在Hask上定义了一个endofunctor,但它甚至不足以描述所有这样的endofunctor.
但是我们使用的实际自然变换有类型:
a - > ma
ma - >(a - > mb) - > mb
这些一般形式的子集是否在上面？为什么它们会自然变换？
嗯,不,他们不是.自然变换大致是函子之间的函数(不是函子).指定monad M的两个自然变换看起来像I -> M我是身份仿函数,M ? M -> M其中?是functor组合.在Haskell中,我们没有直接使用真正的身份函子或函子组合的好方法.相反,我们丢弃身份仿函数以获得(Functor m) => a -> m a第一个,并写出嵌套类型构造函数应用程序和(Functor m) => m (m a) -> m a第二个.
其中第一个显然是return; 第二个是被调用的函数join,它不是类型类的一部分.但是,join可以用来编写,(>>=)后者在日常编程中更常用.
至于具体的monad,如果你想要更多的数学描述,这里是一个例子的快速草图:
对于某些固定类型S,考虑两个函子F和G,其中F(x)=(S,x)和G(x)= S - > x(应该很明显这些是确实有效的函子).
这些仿函数也是邻接的; 考虑自然变换unit :: x -> G (F x)和counit :: F (G x) -> x.扩展定义给了我们unit :: x -> (S -> (S, x))和counit :: (S, S -> x) -> x.这些类型表明无功能应用和元组结构; 随意验证那些工作是否符合预期.
一个adjunction通过函子的组合产生一个monad,所以取G GF并扩展定义,我们得到G(F x)= S - >(S,x),这是Statemonad 的定义.所述unit用于红利当然return; 你应该能够counit用来定义join.
Dav*_*ner 10
粗略地说,Haskell只在一个类别中进行类别理论,其对象是Haskell类型,其箭头是这些类型之间的函数.它绝对不是用于建模类别理论的通用语言.
(数学)仿函数是将一个类别中的事物转换为另一个类别中的事物,可能完全不同的类别的操作.然后,endofunctor是一个仿函数,恰好具有相同的源和目标类别.在Haskell中,仿函数是一种操作,它将Haskell类型中的东西转换为Haskell类型中的其他东西,因此它始终是一个endofunctor.
[如果您遵循数学文献,从技术上讲,操作'(a-> b) - >(ma - > mb)'只是endofunctor m 的箭头部分,'m'是对象部分 ]
当Haskellers谈论"以monad"工作时,他们真的意味着在monad的Kleisli类别中工作.一个monad的Kleisli类别起初是一个彻头彻尾的混乱的野兽,通常需要至少两种颜色的墨水来给出一个很好的解释,所以采取以下尝试,并检查一些参考(不幸的是,维基百科在这里没用除了直接的定义外.
假设你在Haskell类型的C类上有一个monad'm'.其Kleisli类别Kl(m)具有与C相同的对象,即Haskell类型,但是K1(m)中的箭头a~(f)〜> b是箭头a - (f) - > mb in C.(I在我的Kleisli箭头中使用了一条波浪线来区分两者.重申一下:Kl(C)的对象和箭头也是C的对象和箭头,但是箭头指向Kl(C)中的不同对象而不是C.如果这不会让你感到奇怪,请再读一遍小心!
具体来说,考虑一下Maybe monad.它的Kleisli类别只是Haskell类型的集合,它的箭头a~(f)〜> b是函数a - (f) - >也许b.或者考虑(状态s)monad,其箭头a~(f)〜> b是函数a - (f) - >(状态sb)== a - (f) - >(s - >(s,b)) .在任何情况下,你总是写一个波浪形的箭头作为你的函数的codomain类型做一些事情的简写.
[注意State不是monad,因为State的类型是* - >* - >*,所以你需要提供一个类型参数来把它变成数学monad.
到目前为止,这么好,希望如此,但是假设你想要组成箭头a~(f)〜> b和b~(g)〜> c.这些实际上是Haskell函数a - (f) - > mb和b - (g) - > mc,由于类型不匹配,你无法编写.数学解决方案是使用monad的'乘法'自然变换u:mm-> m,如下:a~(f)〜> b~(g)〜> c == a - (f) - > mb - (mg) - > mmc - (u_c) - > mc得到箭头a-> mc,根据需要是Kleisli箭头a~(f; g)〜> c.
也许一个具体的例子有助于此.在Maybe monad中,你不能编写函数f:a - >也许b和g:b - >也许c直接,但是通过将g提升到
Maybe_g :: Maybe b -> Maybe (Maybe c)
Maybe_g Nothing = Nothing
Maybe_g (Just a) = Just (g a)
并使用'明显'
u :: Maybe (Maybe c) -> Maybe c
u Nothing = Nothing
u (Just Nothing) = Nothing
u (Just (Just c)) = Just c
你可以形成一个u . Maybe_g . f功能组合- >你想要的c.
在(State s)monad中,它是相似但更混乱的:给定两个monadic函数a~(f)〜> b和b~(g)〜> c,它们实际上是 - (f) - >(s - >(s ,b))和b - (g) - >(s - >(s,c))在引擎盖下,你把它们举起来组成它们
State_s_g :: (s->(s,b)) -> (s->(s,(s->(s,c))))
State_s_g p s1 = let (s2, b) = p s1 in (s2, g b)
然后你应用'乘法'自然变换u,即
u :: (s->(s,(s->(s,c)))) -> (s->(s,c))
u p1 s1 = let (s2, p2) = p1 s1 in p2 s2
哪种(有点)将最终状态f插入到初始状态g.
在Haskell中,这实际上是一种不自然的工作方式,所以相反,它的(>>=)功能基本上与你做同样的事情,但是以一种更容易实现和使用的方式.这很重要: (>>=)不是"你"的自然转变.你可以用另一个来定义每一个,所以它们是等价的,但它们不是同一个东西.编写了'u'的Haskell版本join.
Kleisli类别定义中缺少的另一个问题是每个对象的身份:a~(1_a)〜> a实际上是 - (n_a) - > ma其中n是'单位'自然变换.这是用returnHaskell 编写的,似乎并没有造成太大的混乱.
在我来到Haskell之前,我学习了类别理论,而且我也很难解决数学家称之为monad的问题与他们在Haskell中的样子之间的不匹配.从另一个方向来看并不容易!
我不确定我理解的是什么问题,但是,你是对的,Haskell中的monad被定义为三元组:
m :: * -> * -- this is endofunctor from haskell types to haskell types!
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
但是类别理论的共同定义是另一个三重:
m :: * -> *
return :: a -> m a
join :: m (m a) -> m a
这有点令人困惑,但要证明这两个定义是平等的并不难.要做到这一点,我们需要定义join来讲(>>=)(反之亦然).第一步:
join :: m (m a) -> m a
join x = ?
这给了我们x :: m (m a).
对于具有类型的东西我们可以做的m _就是aply(>> =)到它:
(x >>=) :: (m a -> m b) -> m b
现在我们需要一些东西作为(>> =)的第二个参数,而且,从我们有约束的连接类型(x >>= y) :: ma.
所以y这里有类型y :: ma -> ma,id :: a -> a非常适合:
join x = x >>= id
(>>=) :: ma -> (a -> mb) -> m b
(>>=) x y = ?
哪里x :: m a和y :: a -> m b.为了得到m b从x和y我们需要的类型的东西a.
不幸的是,我们无法提取a从m a.但是我们可以用它代替其他东西(记住,monad也是一个仿函数):
fmap :: (a -> b) -> m a -> m b
fmap y x :: m (m b)
它非常适合作为参数join:(>>=) x y = join (fmap y x).