免费的 monads 也可以快速应用吗？

Question

我想我为 Free.

想出了一个有趣的 "zippy" Applicative 实例

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 实例，即 "substitutey" 而不是 "zippy"。）

Answer 1

来自definition of Applicative：

If f is also a Monad, it should satisfy

pure = return

(<*>) = ap

(*>) = (>>)

所以这个实现会违反必须与Monad实例一致的应用法则。

也就是说，没有理由你不能为 FreeMonad 提供一个没有 monad 实例但确实有上述应用实例的新类型包装器

newtype Zip f a = Zip { runZip :: FreeMonad f a }
  deriving Functor

instance Applicative f => Applicative (Zip f) where -- ...

Answer 2

是，看来这是合法的Applicative。奇怪！

如，可以读出恒等、同态和互换法律立即来自定义。唯一棘手的是组合定律。

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

有八个案例要检查，请系好安全带。

一个案例有三个 Return：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 中看到正式证明（尽管我怀疑 termination/positivity 检查器可能会把它搞砸）。

Answer 3

为了完整起见，我将使用这个答案来扩展 :

Though I didn't actually write down the proof, I believe the mixed-Free-and-Return cases of the composition law must hold due to parametricity. I also suspect that should be easier to show using the monoidal presentation.

这里Applicative实例的幺半群表示是：

unit = Return ()

Return x *&* v = (x,) <$> v
u *&* Return y = (,y) <$> u
-- I will also piggyback on the `Compose` applicative, as suggested above.
Free u *&* Free v = Free (getCompose (Compose u *&* Compose v))

在幺半群表示下，composition/associativity定律是：

(u *&* v) *&* w ~ u *&* (v *&* w)

现在让我们考虑其中一种混合情况；例如，Free-Return-Free 一个：

(Free fu *&* Return y) *&* Free fw ~ Free fu *&* (Return y *&* Free fw)

(Free fu *&* Return y) *&* Free fw -- LHS
((,y) <$> Free fu) *&* Free fw

Free fu *&* (Return y *&* Free fw) -- RHS
Free fu *&* ((y,) <$> Free fw)

让我们仔细看看这个左侧。 (,y) <$> Free fu 将 (,y) :: a -> (a, b) 应用到 Free fu :: FreeMonad f a 中找到的 a 值。参数化（或更具体地说，(*&*) 的自由定理）意味着我们在使用 (*&*) 之前或之后执行此操作并不重要。这意味着左侧为：

first (,y) <$> (Free fu *&* Free fw)

类似地，右侧变为：

second (y,) <$> (Free fu *&* Free fw)

由于 first (,y) :: (a, c) -> ((a, b), c) 和 second (y,) :: (a, c) -> (a, (b, c)) 相同直到重新关联对，我们有：

first (,y) <$> (Free fu *&* Free fw) ~ second (y,) <$> (Free fu *&* Free fw)
-- LHS ~ RHS

其他混合情况类推。有关证明的其余部分，请参阅 .

免费的 monads 也可以快速应用吗？

Are free monads also zippily applicative?

monads

tree

haskell

applicative

free-monad