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.
Return
s: pure (.) <*> Return f <*> Return g <*> Return z
(.)
.Free
:
pure (.) <*> Free u <*> Return g <*> Return z
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
fmap (f . g) (Free w)
, so follows from the functor law.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.
Free
s: pure (.) <*> Free u <*> Free v <*> Free w
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).
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.
From the definition of Applicative
:
If
f
is also aMonad
, 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 -- ...
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With