Monad法律适用于基于应用的公式

Question

通常在Haskell我们定义Monad来讲小号return和>>=.有时分解>>=成fmap和方便join.Monad一旦你习惯了这两种配方的法律是众所周知的,并且相当直观.

根据仿Applicative函数,还有另一种定义monad的方法:

class Applicative f => MyMonad f where
    myJoin :: f (f a) -> f a

我想知道这种配方的法律.显然,我们可以调整fmap+ join法则,如下所示(我不确定这些名称是否特别贴切,但是很好):

myJoin . myJoin = myJoin . (pure myJoin <*>)       ('Associativity')
myJoin . pure   = myJoin . (pure pure   <*>) = id  ('Identity')

显然,这些条件足以对pure,(<*>)和myJoin以形成单子(在这个意义上,它们保证m `myBind` f = myJoin (pure f <*> m)将成为一个行为良好>>=).但它们也是必要的吗？似乎至少可能的是,Applicative支持上下的额外结构Functor可能允许我们简化这些法则 - 换句话说,上述法律的某些特征可能是非常的,因为已知pure并且(<*>)已经满足Applicative法律.

(如果你想知道为什么我们甚至会遇到困扰这个公式的两种标准可能性:我不确定它在编程环境中是否有用或显而易见,但事实证明是所以当你使用Monads 做自然语言语义时.)

Answer 1

恒等律更容易编写

join . fmap pure = join . pure = id

传统的单子权利同一律直接遵循 的定义>>=。左恒等法Applicative用法

m >>= k = join (fmap k m)

-- proof for right identity
m >>= return       = m
join (fmap pure m) = m  -- definition of >>=
id m               = m  -- identity
m                  = m  -- definition of id

-- proof for left identity
return a >>= f         = f a
join (fmap f (pure a)) = f a  -- definitions of >>= and return
join (pure (f a))      = f a  -- fmap f . pure = pure . f
id (f a)               = f a  -- identity
f a                    = f a  -- definition of id

Applicative和之间的关系的有趣定律Monad是

(<*>) = ap
-- or
m1 <*> m2 = m1 >>= (\x1 -> m2 >>= \x2 -> return (x1 x2)) -- definition of ap

Applicative就join这而言

m1 <*> m2 = join (fmap (\x1 -> fmap x1 m2) m1)
-- proof
m1 <*> m2 = join (fmap (\x1 -> m2 >>= \x2 -> return (x1 x2)) m1)            -- definition of ap
m1 <*> m2 = join (fmap (\x1 -> join (fmap (\x2 -> return (x1 x2)) m2)) m1)  -- definition of >>=
m1 <*> m2 = join (fmap (\x1 -> join (fmap (\x2 -> pure (x1 x2)) m2)) m1)    -- return = pure
m1 <*> m2 = join (fmap (\x1 -> join (fmap (pure . x1) m2)) m1)                 
m1 <*> m2 = join (fmap (\x1 -> join (fmap pure (fmap x1 m2))) m1)           -- fmap (f . g) = fmap f . fmap g
m1 <*> m2 = join (fmap (\x1 -> fmap x1 m2) m1)                              -- identity

可能有一种更优雅的方式来写这个。

我还没有找到一种方法来证明 是Monad基于关联的

• Functor和Applicative法律 - 特别是组成<*>
• 身份join . fmap pure = join . pure = id
• (<*>) = ap

我不确定这是否属实。我认为你需要结合律join . join = join . fmap join