Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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".)

like image 280
Benjamin Hodgson Avatar asked Mar 13 '19 18:03

Benjamin Hodgson


3 Answers

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).

like image 165
Benjamin Hodgson Avatar answered Nov 12 '22 06:11

Benjamin Hodgson


For the sake of completeness, I will use this answer to expand on my comment above:

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.

The monoidal presentation of the Applicative instance here is:

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))

Under the monoidal presentation, the composition/associativity law is:

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

Now let's consider one of its mixed cases; say, the Free-Return-Free one:

(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)

Let's have a closer look at this left-hand side. (,y) <$> Free fu applies (,y) :: a -> (a, b) to the a values found in Free fu :: FreeMonad f a. Parametricity (or, more specifically, the free theorem for (*&*)) means that it doesn't matter if we do that before or after using (*&*). That means the left-hand side amounts to:

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

Analogously, the right-hand side becomes:

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

Since first (,y) :: (a, c) -> ((a, b), c) and second (y,) :: (a, c) -> (a, (b, c)) are the same up to reassociation of pairs, we have:

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

The other mixed cases can be dealt with analogously. For the rest of the proof, see Benjamin Hodgson's answer.

like image 33
duplode Avatar answered Nov 12 '22 06:11

duplode


From the definition of Applicative:

If f is also a Monad, it should satisfy

  • pure = return

  • (<*>) = ap

  • (*>) = (>>)

So this implementation would break the applicative laws that say it must agree with the Monad instance.

That said, there's no reason you couldn't have a newtype wrapper for FreeMonad that didn't have a monad instance, but did have the above applicative instance

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

instance Applicative f => Applicative (Zip f) where -- ...
like image 3
rampion Avatar answered Nov 12 '22 06:11

rampion