# FunctorFix

Levent Erkok erkokl at gmail.com
Sat Sep 9 18:57:32 UTC 2017

```Hi Wolfgang:

Your variant of right-shrinking is an interesting one, and I do suspect it
axioms, since it is violated by at least the strict state monad and the IO
monad. See below code for a demo. It would be interesting to classify
exactly under which conditions it holds, as it does seem weaker than
right-shrinking, but perhaps not by much as you originally suspected.

Cheers,

-Levent.

import Data.IORef

lhs, rhs :: MonadFix m => (a -> m a) -> m b -> m (a, b)
lhs f g = mfix (\ ~(x, _) -> liftM2 (,) (f x) g)
rhs f g = liftM2 (,) (mfix f) g

checkST :: IO ()
checkST = do print \$ (take 10 . fst . fst) \$ runState (rhs f g) []
print \$ (take 10 . fst . fst) \$ runState (lhs f g) []
where f :: [Int] -> State [Int] [Int]
f xs = do let xs' = 1:xs
put xs'
return xs'

g :: State [Int] Int
g = do s <- get
case s of
[x] -> return x
_   -> return 1

checkIO :: IO ()
checkIO = do cl <- newIORef []
print =<< (take 10 . fst) `fmap` rhs (f cl) (g cl)
cr <- newIORef []
print =<< (take 10 . fst) `fmap` lhs (f cr) (g cr)
where f :: IORef [Int] -> [Int] -> IO [Int]
f c xs = do let xs' = 1:xs
writeIORef c xs'
return xs'

g :: IORef [Int] -> IO Int
g c = do s <- readIORef c
case s of
[x] -> return x
_   -> return 1

On Fri, Sep 8, 2017 at 5:27 PM, Wolfgang Jeltsch <wolfgang-it at jeltsch.info>
wrote:

> I see that a general right shrinking axiom would be a bad idea as it
> would rule out many sensible instances of MonadFix. However, I think
> that it is very reasonable to have the following restricted right
> shrinking axiom:
>
>     mfix (\ ~(x, _) -> liftM2 (,) (f x) g) = liftM2 (,) (mfix f) g
>
> The important difference compared to general right shrinking is that the
> shape (or effect) of g does not depend on the output of f x.
>
> axioms? At the moment, it does not look to me that it would.
>
> makes sense not only for all monads, but for all applicative functors.
>
> All the best,
> Wolfgang
>
> Am Donnerstag, den 07.09.2017, 10:11 -0500 schrieb Jonathan S:
> > Your right shrinking law is almost exactly the (impure) right
> > shrinking law specified in Erkok's thesis on page 22, equation 2.22.
> > The problem with this law, as shown on page 56, is that most of the
> > law. In general (see Proposition 3.1.6 on page 27), if (>>=) is strict
> > in its left argument then either the monad is trivial or right
> > shrinking is not satisfied.
> >
> > On Wed, Sep 6, 2017 at 9:21 PM, David Feuer <david.feuer at gmail.com>
> > wrote:
> > >
> > > I think you'll at least have to specify that g is lazy, because f
> > > may let its argument "leak" arbitrarily into the return value of the
> > > action it produces. But I don't have a clear sense of whether this
> > > is a good law otherwise.
> > >
> > > On Sep 6, 2017 10:04 PM, Wolfgang Jeltsch wrote:
> > >
> > >
> > > While we are at pure right shrinking, let me bring up another
> > > question: Why is there no general right shrinking axiom for
> > > MonadFix? Something like the following:
> > >
> > > Right Shrinking:
> > >
> > >     mfix (\ ~(x, _) -> f x >>= \ y -> g y >>= \z -> return (y, z)) >>=
> return . snd
> > >     =
> > >     mfix f >>= g
> > >
> > > Can this be derived from the MonadFix axioms? Or are there
> > > reasonable MonadFix instances for which it does not hold?
> > >
> > > All the best,
> > > Wolfgang
> _______________________________________________
> Libraries mailing list