Are free monads also zippily applicative?

I think I've come up with an interesting "zippy" Applicative instance for 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

It's sort of a zip-longest strategy. For example, using data Pair r = Pair r r as the functor (so FreeMonad Pair is an externally labelled binary tree):

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

I haven't seen anyone mention this instance before. Does it break any Applicative laws? (It doesn't agree with the usual Monad instance of course, which is "substitutey" rather than "zippy".)

Yes, it looks like this is a lawful Applicative. Weird!

As @JosephSible points out, you can read off the identity, homomorphism and interchange laws immediately from the definitions. The only tricky one is the composition law.

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

There are eight cases to check, so strap in.

• One case with three Returns: pure (.) <*> Return f <*> Return g <*> Return z
  • Follows trivially from associativity of (.).
• Three cases with one Free:
  • pure (.) <*> Free u <*> Return g <*> Return z
    • Working backwards from Free u <*> (Return g <*> Return z) you get fmap (\f -> f (g z)) (Free u), so this follows from the functor law.

  • 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
    • Reduces immediately to fmap (f . g) (Free w), so follows from the functor law.
• Three cases with one 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.
    

• Three Frees: pure (.) <*> Free u <*> Free v <*> Free w
  • This case only exercises the Free/Free case of <*>, whose right-hand side is identical to that of Compose's <*>. So this one follows from the correctness of Compose's instance.

For the pure (.) <*> Free u <*> Free v <*> Return z case I used a lemma:

Lemma: 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.

Variously I'm using functor and applicative laws under the induction hypothesis.

This was pretty fun to prove! I'd love to see a formal proof in Coq or Agda (though I suspect the termination/positivity checker might mess it up).