<html><head></head><body><div>Hi, Levent!</div><div><br></div><div>I see the point: Data can be communicated from the first argument of (>>=) to the second not only through the output of the first argument, but also by the first argument storing the data as part of some state and the second argument fetching it from there.</div><div><br></div><div>All the best,</div><div>Wolfgang</div><div><br></div><div>Am Samstag, den 09.09.2017, 11:57 -0700 schrieb Levent Erkok:</div><blockquote type="cite"><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 type="cite">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><br></blockquote></div><br></div>
</blockquote></body></html>