haskell - 基于应用的表述的单子(monad)定律

Question

通常在 Haskell 中我们定义 Monad s 表示为 return和>>= 。有时分解也方便>>=进入fmap和join 。 Monad一旦您习惯了这两种公式的定律，它们是众所周知的并且相当直观。

还有另一种定义 monad 的方法，即 Applicative仿函数:

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形成一个单子(monad)(从某种意义上说，它们保证 m `myBind` f = myJoin (pure f <*> m) 将是一个行为良好的 >>= )。 但是它们也有必要吗？看起来至少有可能 Applicative 的附加结构支持超越 Functor可能允许我们简化这些定律——换句话说，鉴于已知pure，上述定律的某些特征可能是多余的。和(<*>)已经满足Applicative法律。

(如果您想知道为什么我们会在考虑到两种标准可能性中的任何一个的情况下费尽心思去考虑这个公式:我不确定它在编程上下文中是否有用或明显，但它变成了当您使用 Monad 到 do natural langauge semantics 时就会出现这种情况。)

Answer 1

恒等律更容易编写

join . fmap pure = join . pure = id

传统的单子(monad)权利身份法直接遵循 >>= 的定义。左恒等法则使用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