时间戳

首页 > 解决方案 > 免费的单子也适用吗？

haskell - 免费的单子也适用吗？

问题描述

我想我想出了一个有趣的“zippy”Applicative实例Free。

data FreeMonad f a = Free (f (FreeMonad f a))
                   | Return a

instance Functor f => Functor (FreeMonad f) where
    fmap f (Return x) = Return (f x)
    fmap f (Free xs) = Free (fmap (fmap f) xs)

instance Applicative f => Applicative (FreeMonad f) where
    pure = Return

    Return f <*> xs = fmap f xs
    fs <*> Return x = fmap ($x) fs
    Free fs <*> Free xs = Free $ liftA2 (<*>) fs xs

这是一种拉链最长的策略。例如，data Pair r = Pair r r用作函子（FreeMonad Pair外部标记的二叉树也是如此）：

    +---+---+    +---+---+               +-----+-----+
    |       |    |       |      <*>      |           |
 +--+--+    h    x   +--+--+    -->   +--+--+     +--+--+
 |     |             |     |          |     |     |     |
 f     g             y     z         f x   g x   h y   h z

我之前没有看到有人提到过这个例子。它是否违反任何Applicative法律？（当然，它不同意通常的Monad例子，即“替代”而不是“zippy”。）

标签： haskelltreemonadsapplicativefree-monad

解决方案

是的，看起来这是合法的Applicative。诡异的！

正如@JosephSible 指出的那样，您可以立即从定义中读取恒等、同态和交换定律。唯一棘手的是组合法。

pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

有八个箱子要检查，所以请系好安全带。

  • 三个Returns的一个案例：pure (.) <*> Return f <*> Return g <*> Return z
    • 微乎其微地遵循 的关联性(.)。
  • 三例一Free：
    • pure (.) <*> Free u <*> Return g <*> Return z
      • Free u <*> (Return g <*> Return z)从你得到向后工作fmap (\f -> f (g z)) (Free u)，所以这遵循函子定律。
    • pure (.) <*> Return f <*> Free v <*> Return z
fmap ($z) $ fmap f (Free v)
fmap (\g -> f (g z)) (Free v)                  -- functor law
fmap (f . ($z)) (Free v)
fmap f (fmap ($z) (Free v))                    -- functor law
Return f <$> (Free v <*> Return z)             -- RHS of `<*>` (first and second cases)
QED
    • pure (.) <*> Return f <*> Return g <*> Free w
      • 立即减少为fmap (f . g) (Free w)，因此遵循函子定律。
  • 三例一Return： 
    • pure (.) <*> Return f <*> Free v <*> Free w
Free $ fmap (<*>) (fmap (fmap (f.)) v) <*> w
Free $ fmap (\y z -> fmap (f.) y <*> z) v <*> w                  -- functor law
Free $ fmap (\y z -> fmap (.) <*> Return f <*> y <*> z) v <*> w  -- definition of fmap, twice
Free $ fmap (\y z -> Return f <*> (y <*> z)) v <*> w             -- composition
Free $ fmap (\y z -> fmap f (y <*> z)) v <*> w                   -- RHS of fmap, definition of liftA2
Free $ fmap (fmap f) $ fmap (<*>) v <*> w                        -- functor law, eta reduce
fmap f $ Free $ liftA2 (<*>) v w                                 -- RHS of fmap
Return f <*> Free v <*> Free w                                   -- RHS of <*>
QED.

    • pure (.) <*> Free u <*> Return g <*> Free w
Free ((fmap (fmap ($g))) (fmap (fmap (.)) u)) <*> Free w
Free (fmap (fmap (\f -> f . g) u)) <*> Free w                    -- functor law, twice
Free $ fmap (<*>) (fmap (fmap (\f -> f . g)) u) <*> w
Free $ fmap (\x z -> fmap (\f -> f . g) x <*> z) u <*> w         -- functor law
Free $ fmap (\x z -> pure (.) <*> x <*> Return g <*> z) u <*> w
Free $ fmap (\x z -> x <*> (Return g <*> z)) u <*> w             -- composition
Free $ fmap (<*>) u <*> fmap (Return g <*>) w                    -- https://gist.github.com/benjamin-hodgson/5b36259986055d32adea56d0a7fa688f
Free u <*> fmap g w                                              -- RHS of <*> and fmap
Free u <*> (Return g <*> w)
QED.

    • pure (.) <*> Free u <*> Free v <*> Return z
Free (fmap (<*>) (fmap (fmap (.)) u) <*> v) <*> Return z
Free (fmap (\x y -> fmap (.) x <*> y) u <*> v) <*> Return z        -- functor law
Free $ fmap (fmap ($z)) (fmap (\x y -> fmap (.) x <*> y) u <*> v)
Free $ liftA2 (\x y -> (fmap ($z)) (fmap (.) x <*> y)) u v         -- see Lemma, with f = fmap ($z) and g x y = fmap (.) x <*> y
Free $ liftA2 (\x y -> fmap (.) x <*> y <*> Return z) u v          -- interchange
Free $ liftA2 (\x y -> x <*> (y <*> Return z)) u v                 -- composition
Free $ liftA2 (\f g -> f <*> fmap ($z) g) u v                      -- interchange
Free $ fmap (<*>) u <*> (fmap (fmap ($z)) v)                       -- https://gist.github.com/benjamin-hodgson/5b36259986055d32adea56d0a7fa688f
Free u <*> Free (fmap (fmap ($z)) v)
Free u <*> (Free v <*> Return z)
QED.
  • 三个Frees：pure (.) <*> Free u <*> Free v <*> Free w
    • 本例仅练习 的Free/Free情况<*>，其右侧与Compose' 的右侧相同<*>。Compose所以这个是从' 实例的正确性得出的。

对于pure (.) <*> Free u <*> Free v <*> Return z我使用引理的情况：

引理：fmap f (fmap g u <*> v) = liftA2 (\x y -> f (g x y)) u v。

fmap f (fmap g u <*> v)
pure (.) <*> pure f <*> fmap g u <*> v  -- composition
fmap (f .) (fmap g u) <*> v             -- homomorphism
fmap ((f .) . g) u <*> v                -- functor law
liftA2 (\x y -> f (g x y)) u v          -- eta expand
QED.

我在归纳假设下以各种方式使用函子和应用定律。

证明这很有趣！我很想在 Coq 或 Agda 中看到正式的证明（尽管我怀疑终止/积极性检查器可能会搞砸）。

推荐阅读