In my last post, I explored the problem of Applicative effects in free monads. After some great discussion between Edward Kmett, Dave Menendez, /u/MitchellSalad, and myself, I think I’ve come to a new understanding.
For reference, here’s my “free monad given an applicative.”
data Free f a where Pure :: a -> Free f a Free :: f (Free f a) -> Free f a instance Functor f => Functor (Free f) where fmap f (Pure a) = Pure (f a) fmap f (Free a) = Free (fmap (fmap f) a) instance Applicative f => Applicative (Free f) where pure = Pure Pure f <*> a = fmap f a Free f <*> Pure a = Free $ fmap (fmap ($ a)) f Free f <*> Free a = Free (fmap (<*>) f <*> a) instance Applicative f => Monad (Free f) where Pure a >>= k = k a Free a >>= k = Free (fmap (>>= k) a)
The core of the issue is that under my implementation,
(<*>) was purposefully different than
Turns out, it’s a law that
(<*>) must be morally equivalent to
So if the two turn out effectively different, that’s illegal.
Dave Menendez gave a good counter example to the original post using
instance Monoid m => Applicative (Const m) where pure _ = mempty Const f <*> Const v = Const (f `mappend` v) liftFree (Const "a") <*> liftFree (Const "b") = Free (Const "ab") liftFree (Const "a") `ap` liftFree (Const "b") = Free (Const "a")
As you can see,
(<*>) gives a fundamentally different answer than
Cheating on the Ap Test
The truth is,
(<*>) doesn’t have to literally be assigned
(<*>) just has to be morally equivalent to
Const example, morally different results were computed.
But in my original example with Haxl, the results were legal.
The difference is that with
(<*>) is morally different than anything
ap could ever do.
It basically shouldn’t be legal to interpret
Free (Const m).
According to Edward Kmett, it’s all up to interpretation!
The solution is to provide a limited view into
If the interpreter of the free monad agrees to certain laws,
then interpretation can be guaranteed valid.
Essentially, we’re shifting the burden of proof for
(<*>) = ap
to the interpreter.
Let’s recall the Applicative-optimized instance of Applicative for Free.
instance Applicative f => Applicative (Free f) where pure = Pure Pure a <*> Pure b = Pure $ a b Pure a <*> Free mb = Free $ fmap a <$> mb Free ma <*> Pure b = Free $ fmap ($ b) <$> ma Free ma <*> Free mb = Free $ fmap (<*>) ma <*> mb -- <- The important line
In that last line,
(<*>) is used on the
We’re basically asking
f to perform this computation.
So we know that as long as
f is being responsible with
we will get a correct applicative computation.
The question then, is how to use this to make a correct monadic computation?
For a simple example, let’s turn to
This function doesn’t actually need any porting to work with this
retract :: Monad f => Free f a -> f a retract (Pure a) = return a retract (Free as) = as >>= retract
(<*>) = ap in
f, which it has to, then all the work is done for us.
There’s no way to construct a computation that can misuse
f’s monad laws.
But what about examples where
f isn’t a monad?
The simplest way to use these
fs is with
foldFree :: (Functor f, Monad m) => (forall x . f x -> m x) -> Free f a -> m a foldFree _ (Pure a) = return a foldFree f (Free as) = f as >>= foldFree f
In the conventional
Free, the first parameter is a natural transformation.
f, create a corresponding
foldFree will handle the monadic bits.
But this interpreter won’t work with the Applicative-optimized
Well, it will compile and run just fine.
It just won’t produce law-abiding results.
f is actually an Applicative,
(<*>) was used in the computation, it’s possible that the natural
transformation doesn’t correctly transcribe applicative effects.
If this is the case, we don’t know for sure that the
ms returned are correct,
so we don’t know that the result is equivalent to using
That natural transformation has to be something stronger.
It has to preserve the meaning of applicative computations between
So it needs to be an applicative homomorphism.
That is, it needs to be a natural transformation that obeys these laws.
hm :: (Applicative f, Applicative m) => f x -> m x hm (pure a) = pure a hm (f <*> g) = hm f <*> hm g
In code, the only change we can make is strengthening that
foldFree :: (Applicative f, Monad m) => (forall x . f x -> m x) -> Free f a -> m a foldFree _ (Pure a) = return a foldFree f (Free as) = f as >>= foldFree f
We just have to take for granted that the user is supplying
a natural transformation that obeys those laws.
If it does,
then we know that the meanings of applicative computations are being preserved.
Then, as with
retract, the rest is properly guaranteed by the monad laws.
Back to Freer
So what about the
Considering, once again, that we have a free applicative,
which takes any type of kind
* -> *,
we can get the freer monad the same way as before.
type Freer f = Free (Ap f)
Now the interpreter’s job is to take
which is effectively a linked list of
and use those
fs to make an applicative homomorphism.
Now, we have a freer monad that turns any
* -> * into a monad,
and allows the interpreter to optimize applicative effects.
It’s still extremely slow.
I plan to look into church encoding it to improve the performance.
But I’m not sure if that will work well with
Anyway, I’m very happy just knowing a solution for this exists.
Let me know if I’ve made any other mistakes.