Re: FunctorFix

10 Sep 2017


      Hi, Levent!
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.
All the best,
Wolfgang
Am Samstag, den 09.09.2017, 11:57 -0700 schrieb Levent Erkok:
...
Hi Wolfgang:
Your variant of right-shrinking is an interesting one, and I do
suspect it holds for monads like Maybe. 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.
Cheers,
-Levent.
import Data.IORef
import Control.Monad.State.Strict
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 
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.
Does this restricted right shrinking follow from the current
MonadFix
axioms? At the moment, it does not look to me that it would.
An interesting fact about this restricted right shrinking is that it
makes sense not only for all monads, but for all applicative
functors.
All the best,
Wolfgang
...
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
...
MonadFix instances we care about do not follow the right shrinking
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 
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
...
...
action it produces. But I don't have a clear sense of whether
Am Donnerstag, den 07.09.2017, 10:11 -0500 schrieb Jonathan S:
the
the
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
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries