zoom in monadic traversals (implement a Monad instance for Zooming)

[Undeceiver]

Please first excuse me if this is something that has already been discussed. I did a brief search both in the general internet and in the issues page at this GitHub, and I did not find anyone suggesting specifically this.

I have a particular interest in a slightly more constrained type of traversals in which I require Monad instead of Applicative. I have specific reasons for that that I'll share if need be, but which are offtopic for this. I understand this is not all that uncommon. For convenience, I have defined this as a type synonym:

type MTraversal s t a b = forall m. Monad m => (a -> m b) -> s -> m t

The problem is, I cannot use these with zoom, because MTraversal is not a LensLike (Zooming m c) because Zooming is not a Monad.

However, I believe there is no real reason for Zooming not to have a Monad instance. Here is the one I came up with (copying the existing Functor and Applicative implementation in Zooming). I am almost entirely sure it is lawful:

newtype MZooming m c a = MZooming { munZooming :: m (c, a) }

instance Monad m => Functor (MZooming m c) where
  fmap f (MZooming m) = MZooming (liftM (fmap f) m)

instance (Monoid c, Monad m) => Applicative (MZooming m c) where
  pure a = MZooming (return (mempty, a))
  MZooming f <*> MZooming x = MZooming $ do
    (a, f') <- f
    (b, x') <- x
    return (a <> b, f' x')

instance (Monoid c, Monad m) => Monad (MZooming m c) where
    return = pure
    (MZooming x) >>= f = MZooming $ do
        (c, a) <- x
        (d, a') <- munZooming (f a)
        return (c <> d, a')

For now I think what I'll do is implement my version of zoom which works with MZooming instead of Zooming, but I think it would be fairly easy to include this in the lens package?

[ekmett]

Your MZooming is (strict) WriterT. So it is perfectly fine to use as a monad. (You can weaken the requirements for your Applicative instance to use just the Applicative instance for m to be a bit more permissive, so that only the Monad instance requires the Monad.)

That said, "monadic lenses" are deliberately out of scope of this package as they aren't compatible with basically any of the other combinators offered by the package or the laws offered herein. Nothing is stopping you from packaging such a beast in a third-party monadic-lens package or the like.

[ncfavier]

I am also currently investigating these "monadic traversals" (I don't like that name because this is a completely different "monadic" than in "monadic lenses"; I called them journeys because they're traversals that may visit the same place multiple times) in the context of reimplementing jq in Haskell, because jq's "path expression" semantics seem to be exactly that: traversals that may get and set the same locations multiple times (consider .[0, 0] += 1). See here for a rough preview of what I'm doing.

There is some related discussion here: https://www.reddit.com/r/haskell/comments/4tfao3/monadic_traversals/

While I can believe that the bimorphic journeys Monad m => (a -> m b) -> s -> m t are equivalent in strength to Traversal s t a b, this is not the case for the monomorphic version (Monad m => (a -> m a) -> s -> m s) because this allows Kleisli-composing journeys sequentially. This is what makes .[0, 0] possible to express as a journey, but not as a traversal.

I don't think I'm expecting anything from lens, just thought I'd chime in. I might make a journey package eventually, if no one suggests a better name.

[Undeceiver]

It took me a while of thinking, reading what you provided and other sources to feel like I understood what you were saying. Please note that I am experienced in Haskell but not really an expert, neither in practice nor in the theoretical background; though I am interested in both.

I understand from what you are saying that a fundamental difference between traditional applicative traversals and journeys with monadic effects is that due to monads allowing you to essentially "flatten" them when applying them (which applicatives don't); then you can visit the same location multiple times without layering multiple times.

I guess this makes sense, and I think that matches the application I had in mind back in 2020.

Ultimately, the discussion is definitely interesting to me academically, but I'm not sure how much Haskell I will go back to doing or how deep I will ever get into these things. ekmett's answer already provided me some context as to why it wasn't part of lens but that I wasn't doing anything stupid or fundamentally inconsistent. If I do go back to doing Haskell and I need to do something similar I'll definitely look out for journeys. Good to have the discussion here for others as well. But I don't feel that I need any additional closure.

If there is one thing I didn't understand is that ekmett, who told me last month that what I was doing wasn't absurd, said 7 years ago in the thread you linked that there were no additional inhabitants of this beast. I guess he meant that many of the other tools in lens cannot be used with it?

[ncfavier]

The claim made in that thread (and which I find perfectly convincing) is that ∀ a b m. Monad m => (a -> m b) -> t a -> m (t b) holds no more power than ∀ a b m. Applicative m => (a -> m b) -> t a -> m (t b), as long as a and b are universally quantified (parametric). The idea is that such a journey could not make use of its continuation monadically, because it can't assume anything about b, and so there's nothing to be done inside m b that could result in an m (m ...). You can make this more formal by switching to the non-van-Laarhoven representation and arguing that ∀ a b. Free (PStore a b) (t b) and ∀ a b. FreeApplicative (PStore a b) (t b) are isomorphic by appealing to parametricity, as @roconnor did.

My counter-claim, though, is that this claim is rather weak, because the journeys I actually want to consider are far from being parametric in a and b; in fact they're as monomorphic as they come: Journey JSON JSON JSON JSON. In this case, I can make use of monadic facilities to implement things that (even lawless) Traversals could not.

I'm curious to know what your original use case for journeys was, if you care to elaborate.

[Undeceiver]

That last question took a while to answer properly (or at least, do a best attempt). It's been a couple of years since I touched it, and it was a very specific reason.

I think now that actually perhaps I didn't need a journey, but it made something I was doing infinitely easier.

Essentially, I wanted to fold over a set of traversals to produce a singular traversal. Reading now, I think this does not require an MTraversal, but is made infinitely easier to do due to it (I was not aware of this 3 years ago). Perhaps because of what you said of visiting each location once.

In order to fold a bunch of traversals into a single traversal that covers all locations, you would need to algebraically guarantee that those locations are isolated, which is... I don't even know how I would tackle that. I'm not sure I can comprehend what that would involve right now.

With an MTraversal, you can just create a Monoid structure and then use fold as if it's nothing (taken from my code):

add_mtraversals :: Semigroup t => MTraversal r t a b -> MTraversal s r a b -> MTraversal s t a b
add_mtraversals t1 t2 f s = (t2 f s) >>= (t1 f)

instance Semigroup s => Semigroup (ReifiedMTraversal' s a) where
    a1 <> a2 = MTraversal (add_mtraversals (runMTraversal a1) (runMTraversal a2))

instance Semigroup s => Monoid (ReifiedMTraversal' s a) where
    mempty = MTraversal (\_ -> return . id)

Now I'm terrified that I'm saying something really stupid here, but I don't think this is at all trivial with regular Traversals. But I found this just now, that seems to address it in a much more sophisticated (and probably correct) way than I was doing, and which seems to suggest you can do it with regular Traversals as long as you have some constraints: https://hackage.haskell.org/package/optics-core-0.4.1.1/docs/Optics-Traversal.html#g:9

I hope that answers your question without saying anything incredibly stupid :)

[ncfavier]

Right, that all makes sense. lens also has adjoin, but it's stowed away in the Unsound module, its implementation involves witchcraft and it is only lawful if you know that all the targets are disjoint.

By contrast, journeys can be adjoined as a first-class operation, but the downside is that the laws are harder to express because monads don't compose...? (I am still trying to understand this)