Proof of concept of ComposedMonad

[johnynek]

This allows us to make a monad for F[G[_]], so if you have Future[Option[_]] or Eval[List[_]].

The constraint is that the inner type has to be traversable.

So far, I did not yet find a way to compose our old friend tailRecM, but I think this is interesting.

[adelbertc]

Pinging @larsrh who I remember had a proof that Traverse is not sufficient for the laws to hold.

[johnynek]

I'll try to find some time to prove what additional constraints we need. Tests passed locally for Eval[Option[_]].

[larsrh]

@adelbertc Wasn't me … But should be easy to find a counterexample using G = List.

[peterneyens]

A counter example by @TomasMikula : https://gitter.im/typelevel/cats?at=5763685752352c840283176a.

[larsrh]

@peterneyens Thanks for resurfacing this. With the consent of @TomasMikula I think we should put that on the @typelevel blog for posterity.

[johnynek]

That is a nice example. It would be interesting to see what additional constraint is needed to make it lawful.

…

On Mon, Dec 12, 2016 at 23:50 Lars Hupel ***@***.***> wrote: @peterneyens <https://github.com/peterneyens> Thanks for resurfacing this. With the consent of @TomasMikula <https://github.com/TomasMikula> I think we should put that on the @typelevel <https://github.com/typelevel> blog for posterity. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#1478 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAEJdmNfwmEXHN8p9MemHgfLrIpzsej_ks5rHmpogaJpZM4K9CE-> .

[TomasMikula]

@LarsH Sure, if you or someone takes time to write a blog post, feel free to use my counter-example. I'm pretty sure it could be reduced, though (in terms of length of some of the lists involved), I just didn't take time to minimize it.

[TomasMikula]

@johnynek

It would be interesting to see what additional constraint is needed to make it lawful.

I think one sufficient condition would be:

Hypothesis: Given G[_]: Traverse: Monad, then the following laws (relating traverse to pure and flatten) are sufficient for the ComposedTraverseMonad[F[_], G[_]] construction to form a monad for any monad F:

// constrains interaction of traverse with pure
def pureTraverse[F[_]: Applicative, A, B](a: A, f: A => F[B]): IsEq[F[G[A]]] =
  a.pure[G].traverse(f) <-> f(a).map(_.pure[G])

// constrains interaction of traverse with flatten
def flattenTraverse[F[_]: Applicative, A, B](gga: G[G[A]], f: A => F[B]): IsEq[F[G[A]]] =
  gga.flatten.traverse(f) <-> gga.traverse(ga => ga.traverse(f)).map(_.flatten)

I have a sketch of a proof, will try to work out the details and write it up properly.

EDIT: I needed an additional requirement:

def traverseFlatMap[F[_]: Monad, A, B, C](ga: G[A], f: A => F[B], g: B => F[C]): IsEq[F[G[A]]] =
  ga.traverse(a => f(a) flatMap g) <-> ga.traverse(f).flatMap(gb => gb.traverse(g))

When F is a commutative monad, this last requirement follows from the other laws.

[djspiewak]

@johnynek Random FYI on prior art here… djspiewak/emm does this by inferring the composition based on type-level computation. TraverseT was an old proposal by @tixxit (references to the PR where the discussion on this happened is scarce, and he has since deleted the branch, but here's a forum link).

Fundamentally, the problems you run into here are very similar to the ones that Haskell's ListT suffers. Non-commutative monads get really weird. Discussion on this issue here.

@TomasMikula Those two laws look extremely promising! However, I suspect the second one is a lot more constraining than it appears on the surface.

[TomasMikula]

@djspiewak

However, I suspect the second one is a lot more constraining than it appears on the surface.

If my hypothesis proves correct, then it would be interesting to find a traversable monad G for which the construction yields a monad for every monad F, yet doesn't satisfy the said law.

[djspiewak]

@TomasMikula No, I think the law is fairly minimally constraining in that regard. My thought is more that the set of lawful instantiations of G[_] is probably quite small.

[TomasMikula]

@djspiewak Then there's still space to explore to constrain G less and F more. (Notice that my proposed laws do not pose any new constraints on F other than what is already needed for traverse, i.e. that F is applicative.)

[TomasMikula]

So I needed an additional requirement (see the edit above), and yeah, instances are scarce. I can see Option, Either and Writer (and the trivial Id).

Also, I wasn't able to prove that the induced applicative was the same as ComposedApplicative, unless I also assumed:

fa.map(a => gb.map(b => (a, b))) <-> gb.map(b => fa.map(a => (a, b))).sequence

which I see as a sort of commutativity between the two distinct types of effects, and is probably even scarcer.

Since my results are uninteresting, it's not worth it to write up the proofs. Monad transformers FTW!

[djspiewak]

which I see as a sort of commutativity between the two distinct types of effects, and is probably even scarcer.

This is precisely the definition of a commutative monad (or rather, a commutative applicative).

[xuwei-k]

TraverseT was an old proposal by @tixxit (references to the PR where the discussion on this happened is scarce, and he has since deleted the branch, but here's a forum link).

https://github.com/scalaz/scalaz/pull/639/files

[xuwei-k]

discussion about commutative monad in scalaz

scalaz/scalaz#921 (comment)

[TomasMikula]

@djspiewak I should have added type annotations: F[_]: Applicative, G[_]: Traverse, fa: F[A], gb: G[B]. This is "commutativity" between two distinct functors, one applicative and one traversable. OTOH, commutative applicative is commutative with itself.

[oscar-stripe]

@TomasMikula if you have the code set up to easily check, it seems to me that when F = Eval, we may have everything we need in some interesting cases. If this is true, it is interesting, because it lets us wrap a monad in an Eval and get stack safety of the recursion.

If that was the case it would be nice to have a recipe to take a G[_]: Monad: Traverse and provide Monad[lambda => F[G[lambda]]]

[TomasMikula]

My proof is "pen and paper". I can try to recapitulate it here.

Given the construction

def nestedMonad[F[_], G[_]](implicit F: Monad[F], G: Monad[G], TG: Traverse[G]): Monad[λ[A => F[G[A]]]] =
  new Monad[λ[A => F[G[A]]]] {
    def pure[A](a: A): F[G[A]] = F.pure(G.pure(a))
    def flatMap[A, B](fga: F[G[A]])(f: A => F[G[B]]): F[G[B]] =
      F.flatMap(fga)(ga => F.map(TG.traverse(ga)(f))(G.flatten))
  }

assuming the usual monad and traverse laws, plus these three additional laws for G

def pureTraverse[F[_]: Applicative, A, B](a: A, f: A => F[B]): IsEq[F[G[A]]] =
  a.pure[G].traverse(f) <-> f(a).map(_.pure[G])

def flattenTraverse[F[_]: Applicative, A, B](gga: G[G[A]], f: A => F[B]): IsEq[F[G[A]]] =
  gga.flatten.traverse(f) <-> gga.traverse(ga => ga.traverse(f)).map(_.flatten)

def traverseFlatMap[F[_]: Monad, A, B, C](ga: G[A], f: A => F[B], g: B => F[C]): IsEq[F[G[A]]] =
  ga.traverse(a => f(a) flatMap g) <-> ga.traverse(f).flatMap(gb => gb.traverse(g))

we need to show that the 3 monad laws (left identity, right identity, associativity) hold for

val FG = nestedMonad[F, G]

Let's also state the "free" naturality law (from https://en.wikibooks.org/wiki/Haskell/Traversable#The_Traversable_laws):

-- If t is an applicative homomorphism, then
t . traverse f = traverse (t . f) -- naturality

and note that F.pure: Id ~> F is an applicative homomorphism (left as an exercise ;)), so we can use this law with t := pure.

(Also note that when F is a commutative monad, then F.flatten: λ[a => F[F[a]]] ~> F is an applicative homomorphism from ComposedApplicative[F, F] to F. This would suffice to remove the traverseFlatMap constraint above (left as an exercise ;)).)

In the proofs below, (!!!) marks places where the new laws are used. Have fun with proof-reading ;)

1. Left identity

To show:

FG.pure(a).flatMap(f) <-> f(a)

Just expand the definition of pure and flatMap from nestedMonad and reduce:

F.pure(G.pure(a)).flatMap(ga => ga.traverse(f).map(_.flatten)) // pure(x).flatMap(h) ---> h(x)
G.pure(a).traverse(f).map(_.flatten)                           // (!!!) apply pureTraverse law
f(a).map(gb => G.pure(gb)).map(_.flatten)                      // compose maps
f(a).map(gb => G.pure(gb).flatten)                             // rewrite flatten in terms of flatMap
f(a).map(gb => G.pure(gb).flatMap(identity))                   // pure(x).flatMap(h) ---> h(x)
f(a).map(gb => identity(gb))
f(a)

2. Right identity

To show:

val fga: F[G[A]]

FG.flatMap(fga)(FG.pure) <-> fga

Again, just expand the definition and reduce the left-hand side:

FG.flatMap(fga)(FG.pure)                                              // expand FG.flatMap
fga.flatMap(ga => ga.traverse(a => FG.pure(a)).map(_.flatten))        // expand FG.pure
fga.flatMap(ga => ga.traverse(a => F.pure(G.pure(a))).map(_.flatten)) // naturality for F.pure
fga.flatMap(ga => F.pure(ga.traverse(a => G.pure(a))).map(_.flatten)) // reassociate flatMap, map
fga.flatMap(ga => F.pure(ga.traverse(a => G.pure(a)))).map(_.flatten) // flatMap(x => pure(f(x))) ---> map(f)
fga.map(ga => ga.traverse(a => G.pure(a))).map(_.flatten)             // naturality for G.pure
fga.map(ga => G.pure(ga.traverse[Id, A](a => a))).map(_.flatten)      // traverseIdentity, i.e. traverse[Id, A](f) ---> map(f)
fga.map(ga => G.pure(ga.map(a => a))).map(_.flatten)                  // ga.map(identity) ---> ga
fga.map(ga => G.pure(ga)).map(_.flatten)                              // compose maps
fga.map(ga => G.pure(ga).flatten)                                     // annihilate pure and flatten
fga.map(ga => ga)
fga

3. Associativity

To show:

val fga: F[G[A]]
val f: A => F[G[B]]
val g: B => F[G[C]]

FG.flatMap(FG.flatMap(fga)(f))(g) <-> FG.flatMap(fga)(a => FG.flatMap(f(a))(g))

Expand and reduce left-hand side:

FG.flatMap(FG.flatMap(fga)(f))(g)                                                             // expand inner FG.flatMap
FG.flatMap(fga.flatMap(ga => ga.traverse(f).map(_.flatten)))(g)                               // expand (outer) FG.flatMap
fga.flatMap(ga => ga.traverse(f).map(_.flatten)).flatMap(gb => gb.traverse(g).map(_.flatten)) // re-associate flatMaps
fga.flatMap(ga => ga.traverse(f).map(_.flatten).flatMap(gb => gb.traverse(g).map(_.flatten))) // compose map and flatMap
fga.flatMap(ga => ga.traverse(f).flatMap(ggb => ggb.flatten.traverse(g).map(_.flatten)))      // (!!!) flattenTraverse
fga.flatMap(ga => ga.traverse(f).flatMap(ggb => ggb.traverse(gb => gb.traverse(g)).map(_.flatten).map(_.flatten))) // re-associate flatMap/map
fga.flatMap(ga => ga.traverse(f).flatMap(ggb => ggb.traverse(gb => gb.traverse(g).map(_.flatten))).map(_.flatten)) // (!!!) traverseFlatMap
fga.flatMap(ga => ga.traverse(a => f(a).flatMap(gb => gb.traverse(g).map(_.flatten))).map(_.flatten)) // recognize definition of FG.flatMap
fga.flatMap(ga => ga.traverse(a => FG.flatMap(f(a))(g)).map(_.flatten))                               // recognize definition of FG.flatMap
FG.flatMap(fga)(a => FG.flatMap(f(a))(g))

[djspiewak]

@TomasMikula This is outstanding work. When I grow up, I want to be as cool as you are.

I guess the path forward would be to see if we can weaken the constraints in any way. flattenTraverse seems very constraining, but traverseFlatMap looks like "literally a commutative monad" to me. That lines up nicely with some of the category theoretical intuitions that @runarorama built a few months ago, but I haven't yet lost hope that there might be a way to narrow it down.

At the very least, we could explore more constraints on F[_].

[TomasMikula]

I guess the path forward would be to see if we can weaken the constraints in any way.

Yup. What I did was just expand the definitions and whenever I couldn't make a step forward, I introduced a new assumption :)

traverseFlatMap looks like "literally a commutative monad" to me.

I formulated it as a requirement on G[_]: Traverse, i.e. given G[_]: Traverse, we require that for all F[_]: Monad: traverseFlatMap holds. If we pose it as a requirement on F, i.e. given F[_]: Monad, we require that for all G[_]: Traverse: traverseFlatMap holds; then F[_] being a commutative monad is sufficient for traverseFlatMap to hold. It would be interesting to find out whether it is also necessary.

[milessabin]

being a commutative monad is sufficient for traverseFlatMap to hold. It would be interesting to find out whether it is also necessary.

I don't want to spoil anyone's fun, but surely this is well explored territory by now ... hasn't someone established this one way or another already?

If not then someone has an ICFP paper or two in the making :-)

[djspiewak]

I don't want to spoil anyone's fun, but surely this is well explored territory by now ... hasn't someone established this one way or another already?

If they have, they've hidden it very well from Google. That's not to say it doesn't exist or that I couldn't have spent more time hunting it in the past few years, but I've been looking for this stuff on-and-off for five or six years without success.

[TomasMikula]

surely this is well explored territory by now ... hasn't someone established this one way or another already?

Looking it up ruins all the fun :P

[djspiewak]

Composing Monads (Jones and Duponcheel, 1993) explores this space in some depth. Section 3.4 is particularly interesting, since the function they examine would be called sequence in modern parlance. However, the laws they require for prod and dorp look superficially quite similar to @TomasMikula's, except encoded in terms of map and join.

[johnynek]

@djspiewak that paper is a nice find.

It seems, though I didn't do all the work, that we should be able to find interesting cases of composition for λ[a => Eval[F[a]]]. I think that will be interesting if we can explore that, since we should be able to use that to get stack safety for Monad[F].

[djspiewak]

@johnynek Unless I'm very much mistaken, Eval is a commutative monad. So it should satisfy @TomasMikula's laws, implying that λ[a => Eval[F[a]]] forms a valid monad under Traverse. (I could have the composition backwards though)

[TomasMikula]

I have only shown that commutativity of the outer monad is sufficient for the third law (traverseFlatMap) to hold.

[ceedubs]

@johnynek I think that there is wide agreement that this shouldn't be merged in its current form, as further constraints are needed. This PR seems to have stalled. Should we close it out and open an issue to potentially pursue composed monads?

[johnynek]

@ceedubs I'm not sure I agree. Didn't @TomasMikula present a proof here that when certain laws hold this necessarily is a lawful Monad:
#1478 (comment)

The value of this is that tailRecM is implementable in this construction. Note also, there is no implement materializer here. This is opt in.

I'm not sure why this is any different than any other structures we have that are also not lawful at the type-level, but require users to implement them correctly (e.g. Monad, Monoid, etc...) The difference here is that the implementation is always the same in many cases (when certain laws hold that @TomasMikula outlined.

[ceedubs]

@johnynek yes, when certain laws hold, the result is a lawful Monad. But as far as I know, for all of our other type classes, the compose* methods are guaranteed to return lawful instances as long as all of the implicit instances that they require as arguments are lawful. That's not the case with this method in its current form, right?

I would think that you would want to specify those constraints, even if it's via "marker" type classes or something.

[djspiewak]

@johnynek As an exercise, list off some examples which satisfy @TomasMikula's proof. The set is extremely small. So unlike tailRecM, which is only unlawful in a very small and specific subset of monads, ComposedMonad would only be lawful in a very small and specific subset of monads. Most of the time, it would just represent a very subtle and dangerous pitfall.

There just isn't a compelling application for this given the extremely small scope of validity and the relatively incremental gain which comes within that scope.

[johnynek]

The gain is that it always has tailRecM I believe regardless of F or G having one. That's the motivation. You use flatten and traverse to implement it. That is the win. I'll update the PR I guess with a type, the laws and some examples.

…

On Wed, May 17, 2017 at 17:00 Daniel Spiewak ***@***.***> wrote: @johnynek <https://github.com/johnynek> As an exercise, list off some examples which satisfy @TomasMikula <https://github.com/tomasmikula>'s proof. The set is *extremely* small. So unlike tailRecM, which is only unlawful in a very small and specific subset of monads, ComposedMonad would only be *lawful* in a very small and specific subset of monads. Most of the time, it would just represent a very subtle and dangerous pitfall. There just isn't a compelling application for this given the extremely small scope of validity and the relatively incremental gain which comes within that scope. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1478 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAEJdqIYX1-YIgZqGIbg1x9_s_qCPs7vks5r67ROgaJpZM4K9CE-> .

[djspiewak]

@johnynek F and G are monads by constraint, which means they have tailRecM literally by definition. Maybe not a lawful one, but they have it. And for monads F or G where a lawful tailRecM is impossible, ComposedMonad will also be unable to implement one.

I mean, I'll wait to see the laws and examples and such. It would be nice to see something useful come out of all of the work that has been done on composing monads through Traverse. I just don't see it right now.

[larsrh]

I think ultimately this idea doesn't work out very well. I vote for closing this PR.

[LukaJCB]

We can always open this again later :)