FunctorFix

[Wolfgang Jeltsch]

Am Donnerstag, den 07.09.2017, 04:54 +0300 schrieb Wolfgang Jeltsch:
> Am Samstag, den 02.09.2017, 14:08 -0500 schrieb Jonathan S:
> > 
> > I think that in addition to nesting and sliding, we should have the
> > following law:
> > 
> > ffix (\x -> fmap (f x) g) = fmap (\y -> fix (\x -> f x y)) g
> > 
> > I guess I'd call this the "pure left shrinking" law because it is
> > the composition of left shrinking and purity:
>
> I wonder whether “pure left shrinking” is an appropriate name for
> this. The shrinking is on the left, but the purity is on the right.
> Note that in “pure right shrinking”, a derived property discussed in
> Erkok’s thesis, both the shrinking and the purity are on the right.

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