免费的monad也适用于zippily吗？

Question

我想我已经为Applicative提出了一个有趣的“zippy”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”。）

Answer 1

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

作为@JosephSible points out，您可以立即从定义中读出身份，同态和交换法则。唯一棘手的是组成法。

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)，因此遵循仿函法。
• 一个qazxsw poi的三个案例： qazxsw poi qazxsw poi qazxsw poi
• 三个Returns：

  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.

  的Free案例，其右侧与pure (.) <*> Free u <*> Free v <*> Free w的Free相同。所以这一点来自Free实例的正确性。

对于<*>案，我使用了一个引理：

引理：Compose。

<*>

不同，我在归纳假设下使用仿函数和适用法则。

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

Answer 2

为了完整起见，我将使用这个答案来扩展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.

在幺半群呈现下，组成/相关性法则是：

my comment above

现在让我们考虑其中的一个混合案例;比方说，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))

：

(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)之前或之后这样做并不重要。这意味着左侧相当于：

a

类似地，右侧变为：

Free fu :: FreeMonad f a

由于(*&*)和(*&*)在重组关联方面是相同的，我们有：

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

其他混合案例可以类似地处理。对于其余的证明，请参阅second (y,) <$> (Free fu *&* Free fw) 。

Answer 3

来自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

，它应该满足

• Benjamin Hodgson's answer = definition of Applicative
• f = Monad
• pure = return

所以这个实现将打破适用的法律，说它必须与(<*>)实例一致。

也就是说，没有理由你没有一个没有monad实例的ap的newtype包装器，但确实有上面的应用实例

(*>)