Fixed-point of a monadic and comonadic computation

326 Views Asked by At

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?

1

There are 1 best solutions below

7
S.Klumpers On

Yes, in fact, we can define a reasonable wmfix :: w (w a -> m a) -> m a in two different ways; one starting from cofix, and the other from mfix.

If we normalize both approaches, they become roughly the same idea: turn some f : w (w a -> m a) into a suitable b -> b, take the fixpoint, and dig out the m a from b. For the cofix-like approach we can take

wmfix1 f = cofix (fmap ((. distr) . (=<<)) f)

or directly

wmfix1 f = extract (fix g) where
    g :: w (m a) -> w (m a)
    g = extend (\x -> distr x >>= extract f)

If we start from mfix instead, we get

wmfix2 f = fmap extract (extract (fmap (mfix . (distr .)  . extend) f))

or

wmfix2 f = fmap extract (fix h) where
    h :: m (w a) -> m (w a)
    h = (distr . extend (extract f) =<<)

Unfortunately, it doesn't look like these are same in general, which requires a condition like

fmap extract (distr (extend f x)) = f x

This condition does seem to hold for the w = NonEmpty, m = Maybe case you mentioned.