<div dir="ltr">Hi Wolfgang:<div><br></div><div>Your variant of right-shrinking is an interesting one, and I do suspect it holds for monads like <font face="monospace, monospace">Maybe</font>. But it definitely doesn't follow from MonadFix 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.</div><div><br></div><div>Cheers,</div><div><br></div><div>-Levent.</div><div><br></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><div><font face="monospace, monospace">import Data.IORef</font></div></div><div><div><font face="monospace, monospace">import Control.Monad.State.Strict</font></div></div><div><div><font face="monospace, monospace"><br></font></div></div><div><div><font face="monospace, monospace">lhs, rhs :: MonadFix m => (a -> m a) -> m b -> m (a, b)</font></div></div><div><div><font face="monospace, monospace">lhs f g = mfix (\ ~(x, _) -> liftM2 (,) (f x) g)</font></div></div><div><div><font face="monospace, monospace">rhs f g = liftM2 (,) (mfix f) g</font></div></div><div><div><font face="monospace, monospace"><br></font></div></div><div><div><font face="monospace, monospace">checkST :: IO ()</font></div></div><div><div><font face="monospace, monospace">checkST = do print $ (take 10 . fst . fst) $ runState (rhs f g) []</font></div></div><div><div><font face="monospace, monospace"> print $ (take 10 . fst . fst) $ runState (lhs f g) []</font></div></div><div><div><font face="monospace, monospace"> where f :: [Int] -> State [Int] [Int]</font></div></div><div><div><font face="monospace, monospace"> f xs = do let xs' = 1:xs</font></div></div><div><div><font face="monospace, monospace"> put xs'</font></div></div><div><div><font face="monospace, monospace"> return xs'</font></div></div><div><div><font face="monospace, monospace"><br></font></div></div><div><div><font face="monospace, monospace"> g :: State [Int] Int</font></div></div><div><div><font face="monospace, monospace"> g = do s <- get</font></div></div><div><div><font face="monospace, monospace"> case s of</font></div></div><div><div><font face="monospace, monospace"> [x] -> return x</font></div></div><div><div><font face="monospace, monospace"> _ -> return 1</font></div></div><div><div><font face="monospace, monospace"><br></font></div></div><div><div><font face="monospace, monospace">checkIO :: IO ()</font></div></div><div><div><font face="monospace, monospace">checkIO = do cl <- newIORef []</font></div></div><div><div><font face="monospace, monospace"> print =<< (take 10 . fst) `fmap` rhs (f cl) (g cl)</font></div></div><div><div><font face="monospace, monospace"> cr <- newIORef []</font></div></div><div><div><font face="monospace, monospace"> print =<< (take 10 . fst) `fmap` lhs (f cr) (g cr)</font></div></div><div><div><font face="monospace, monospace"> where f :: IORef [Int] -> [Int] -> IO [Int]</font></div></div><div><div><font face="monospace, monospace"> f c xs = do let xs' = 1:xs</font></div></div><div><div><font face="monospace, monospace"> writeIORef c xs'</font></div></div><div><div><font face="monospace, monospace"> return xs'</font></div></div><div><div><font face="monospace, monospace"><br></font></div></div><div><div><font face="monospace, monospace"> g :: IORef [Int] -> IO Int</font></div></div><div><div><font face="monospace, monospace"> g c = do s <- readIORef c</font></div></div><div><div><font face="monospace, monospace"> case s of</font></div></div><div><div><font face="monospace, monospace"> [x] -> return x</font></div></div><div><div><font face="monospace, monospace"> _ -> return 1</font></div></div></blockquote></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Sep 8, 2017 at 5:27 PM, Wolfgang Jeltsch <span dir="ltr"><<a href="mailto:wolfgang-it@jeltsch.info" target="_blank">wolfgang-it@jeltsch.info</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I see that a general right shrinking axiom would be a bad idea as it<br>
would rule out many sensible instances of MonadFix. However, I think<br>
that it is very reasonable to have the following restricted right<br>
shrinking axiom:<br>
<br>
mfix (\ ~(x, _) -> liftM2 (,) (f x) g) = liftM2 (,) (mfix f) g<br>
<br>
The important difference compared to general right shrinking is that the<br>
shape (or effect) of g does not depend on the output of f x.<br>
<br>
Does this restricted right shrinking follow from the current MonadFix<br>
axioms? At the moment, it does not look to me that it would.<br>
<br>
An interesting fact about this restricted right shrinking is that it<br>
makes sense not only for all monads, but for all applicative functors.<br>
<br>
All the best,<br>
Wolfgang<br>
<span class="im HOEnZb"><br>
Am Donnerstag, den 07.09.2017, 10:11 -0500 schrieb Jonathan S:<br>
> Your right shrinking law is almost exactly the (impure) right<br>
> shrinking law specified in Erkok's thesis on page 22, equation 2.22.<br>
> The problem with this law, as shown on page 56, is that most of the<br>
> MonadFix instances we care about do not follow the right shrinking<br>
> law. In general (see Proposition 3.1.6 on page 27), if (>>=) is strict<br>
> in its left argument then either the monad is trivial or right<br>
> shrinking is not satisfied.<br>
><br>
> On Wed, Sep 6, 2017 at 9:21 PM, David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>><br>
> wrote:<br>
> ><br>
> > I think you'll at least have to specify that g is lazy, because f<br>
> > may let its argument "leak" arbitrarily into the return value of the<br>
> > action it produces. But I don't have a clear sense of whether this<br>
> > is a good law otherwise.<br>
> ><br>
</span><div class="HOEnZb"><div class="h5">> > On Sep 6, 2017 10:04 PM, Wolfgang Jeltsch wrote:<br>
> ><br>
> ><br>
> > While we are at pure right shrinking, let me bring up another<br>
> > question: Why is there no general right shrinking axiom for<br>
> > MonadFix? Something like the following:<br>
> ><br>
> > Right Shrinking:<br>
> ><br>
> > mfix (\ ~(x, _) -> f x >>= \ y -> g y >>= \z -> return (y, z)) >>= return . snd<br>
> > =<br>
> > mfix f >>= g<br>
> ><br>
> > Can this be derived from the MonadFix axioms? Or are there<br>
> > reasonable MonadFix instances for which it does not hold?<br>
> ><br>
> > All the best,<br>
> > Wolfgang<br>
______________________________<wbr>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><br>
</div></div></blockquote></div><br></div>