ekmett / free

free monads
http://hackage.haskell.org/package/free
Other
159 stars 65 forks source link

Document 'Control.Monad.Free.Ap' has to work only on "commutative" monads #210

Open viercc opened 2 years ago

viercc commented 2 years ago

I propose updates on the documentation of Control.Monad.Free.Ap module to tell the Free f monad in this module should be interpreted using a commutative (or "morally" commutative) Monad.

The Free f monad in the Control.Monad.Free.Ap module is to provide an optimization for some usages (e.g. Haxl-like monad having concurrent <*>), while it doesn't obey the law requiring (<*>) = ap in the eyes of strict equality.

The current documentation of Control.Monad.Free.Ap module states the loosened law hold under the interpretation of foldFree f if f is an applicative homomorphism. I think it's written as if the following statement is true.

If f is an applicative homomorphism, foldFree f (x <*> y) = foldFree f (x `ap` y)

But it doesn't hold. Let foo, bar be the following values of Free IO monad.

foo :: Free IO (() -> ())
foo = do liftF (putStrLn "foo1")
         liftF (putStrLn "foo2")
         return id

bar :: Free IO ()
bar = do liftF (putStrLn "bar1")
         liftF (putStrLn "bar2")

Then retract (foo <*> bar) and retract (foo `ap` bar) print out strings in different order. Since retract = foldFree id and id :: IO a -> IO a is an applicative homomorphism without doubt, the above statement about the lawfulness of Free f is too optimistic.

Generally, retract (x `ap` y) = retract x `ap` retract y = retract x <*> retract y hold. So the loosened law is equivalent to retract (foo <*> bar) = retract foo <*> retract bar. This is again equivalent to say the monad f in retract :: Free f a -> f a is a commutative monad. In terms of foldFree f, I think "f must be an applicative homomorphism to a commutative monad" is appropriate.

Of course, the primary usage of Haxl-like monad isn't commutative in the strictest sense, but it's "morally" commutative because they're best used when the ordering of effects do not matter.