In Haskell, Given a monad m, there is mfix :: (a -> m a) -> m a that computes the fixed-point of a monadic computation.
Dually, given a comonad w, there is cofix :: w (w a -> a) -> a that computes the fixed-point of a comonadic computations.
Now suppose that I have a program that uses both a monad m and a comonad w that are related by a distributivity law distr :: w (m a) -> m (w a) of the comonad over the monad. Is it possible to combine mfix and cofix into a function of type w (w a -> m a) -> m a that would compute the fixpoint of monadic and comonadic computations?
Yes, in fact, we can define a reasonable
wmfix :: w (w a -> m a) -> m ain two different ways; one starting fromcofix, and the other frommfix.If we normalize both approaches, they become roughly the same idea: turn some
f : w (w a -> m a)into a suitableb -> b, take the fixpoint, and dig out them afromb. For thecofix-like approach we can takeor directly
If we start from
mfixinstead, we getor
Unfortunately, it doesn't look like these are same in general, which requires a condition like
This condition does seem to hold for the
w = NonEmpty, m = Maybecase you mentioned.