FunctorFix

[Wolfgang Jeltsch]

Hi!

Let me summarize the outcomes of this discussion.

The goal is to replace the current MonadFix class by classes FunctorFix,
ApplicativeFix, and MonadFix declared as follows:

> class Functor f => FunctorFix f where
>
>     ffix :: (a -> f a) -> f a
>
> class (Applicative f, FunctorFix f) => ApplicativeFix f where
>
>     afix :: (a -> f a) -> f a
>
> class (Monad m, ApplicativeFix m) => MonadFix m where
>
>     mfix :: (a -> m a) -> m a

Note that the new MonadFix class differs from the previous one by its
additional ApplicativeFix superclass constraint.

For every instance of MonadFix, the equation mfix = afix should hold;
for every instance of ApplicativeFix, the equation afix = ffix should
hold.

All instances of FunctorFix should fulfill the following axioms:

Nesting:

    ffix (\ x -> ffix (\ y -> f x y)) = ffix (\ x -> f x x)

Sliding:

    ffix (fmap h . f) = fmap h (ffix (f . h))

    for strict h

Functorial left shrinking:

    ffix (\ x -> fmap (h x) a) = fmap (\ y -> fix (\ x -> h x y)) a

All instances of ApplicativeFix should additionally fulfill the
following axioms:

Purity:

    ffix (pure . h) = pure (fix h)

Applicative left shrinking:

    afix (\ ~(_, y) -> liftA2 (,) a (g y)) = liftA2 (,) a (afix g)

All instances of MonadFix should additionally fulfill the following
axiom:

Monadic left shrinking:

    mfix (\ x -> a >>= \ y -> f x y) = a >>= \ y -> mfix (\ x -> f x y)

Should I turn this into a formal library proposal?

All the best,
Wolfgang

Am Montag, den 11.09.2017, 03:08 +0300 schrieb Wolfgang Jeltsch:
> In my opinion, ApplicativeFix should have a restricted left shrinking
> axiom that is analogous to the restricted right shrinking axiom I
> proposed in another e-mail in this thread (but which does not hold for
> several MonadFix examples). Restricted Left Shrinking would look as
> follows:
> 
>     afix (\ ~(_, y) -> liftA2 (,) f (g y)) = liftA2 (,) f (afix g)
> 
> I think this axiom is stronger than the one you suggested.
> 
> All the best,
> Wolfgang
> 
> Am Dienstag, den 05.09.2017, 19:35 -0400 schrieb David Feuer:
> > 
> > As long as we're going down this path, we should also consider
> > ApplicativeFix. All the laws except left shrinking make immediate
> > sense in that context. That surely has a law or two of its own. For
> > example, I'd expect that
> > 
> > afix (\x -> a *> f x) = a *> afix f
> > 
> > I don't know if it has anything more interesting.
> > 
> > 
> > On Tue, Sep 5, 2017 at 6:11 PM, Wolfgang Jeltsch
> > <wolfgang-it at jeltsch.info> wrote:
> > > 
> > > 
> > > Jonathan, thanks a lot for working this out. Impressive!
> > > 
> > > So we want the following laws for FunctorFix:
> > > 
> > > Pure left shrinking:
> > > 
> > >     ffix (\x -> fmap (f x) g) = fmap (\y -> fix (\x -> f x y)) g
> > > 
> > > Sliding:
> > > 
> > >     ffix (fmap h . f) = fmap h (ffix (f . h))
> > > 
> > >     for strict h
> > > 
> > > Nesting:
> > > 
> > >     ffix (\x -> ffix (\y -> f x y)) = ffix (\x -> f x x)
> > > 
> > > Levent Erkok’s thesis also mentions a strictness law for monadic
> > > fixed
> > > points, which is not mentioned in the documentation of
> > > Control.Monad.Fix. It goes as follows:
> > > 
> > > Strictness:
> > > 
> > >     f ⊥ = ⊥ ⇔ mfix f = ⊥
> > > 
> > > Does this hold automatically, or did the designers of
> > > Control.Monad.Fix
> > > considered it inappropriate to require this?
> > > 
> > > All the best,
> > > Wolfgang
> > > 
> > > 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:
> > > > 
> > > > ffix (\x -> fmap (f x) g)
> > > > =
> > > > ffix (\x -> g >>= \y -> return (f x y))
> > > > = {left shrinking}
> > > > g >>= \y -> ffix (\x -> return (f x y))
> > > > = {purity}
> > > > g >>= \y -> return (fix (\x -> f x y))
> > > > =
> > > > fmap (\y -> fix (\x -> f x y)) g
> > > > 
> > > > This is powerful enough to prove the scope change law, but is
> > > > significantly simpler:
> > > > 
> > > > ffix (\~(a, b) -> fmap (\a' -> (a', h a' a b)) (f a))
> > > > =
> > > > ffix (\t -> fmap (\a' -> (a', h a' (fst t) (snd t))) (f (fst
> > > > t)))
> > > > = {nesting}
> > > > ffix (\t1 -> ffix (\t2 -> fmap (\a' -> (a', h a' (fst t1) (snd
> > > > t1)))
> > > > (f (fst t2))))
> > > > =
> > > > ffix (\~(a, b) -> ffix (fmap (\a' -> (a', h a' a b)) . f . fst))
> > > > = {sliding}
> > > > ffix (\~(a, b) -> fmap (\a' -> (a', h a' a b)) (ffix (f . fst .
> > > > (\a'
> > > > -> (a', h a' a b)))))
> > > > =
> > > > ffix (\~(a, b) -> fmap (\a' -> (a', h a' a b)) (ffix f))
> > > > = {pure left shrinking}
> > > > fmap (\a' -> fix (\~(a, b) -> (a', h a' a b))) (ffix f)
> > > > 
> > > > Moreover, it seems necessary to prove that ffix interacts well
> > > > with
> > > > constant functions:
> > > > 
> > > > ffix (const a)
> > > > =
> > > > ffix (\_ -> fmap id a)
> > > > =
> > > > fmap (\y -> fix (\_ -> id y)) a
> > > > =
> > > > fmap id a
> > > > =
> > > > a
> > > > 
> > > > In addition, when the functor in question is in fact a monad, it
> > > > implies purity:
> > > > 
> > > > ffix (return . f)
> > > > =
> > > > ffix (\x -> return (f x))
> > > > =
> > > > ffix (\x -> fmap (\_ -> f x) (return ()))
> > > > =
> > > > fmap (\_ -> fix (\x -> f x)) (return ())
> > > > =
> > > > return (fix f)
> > > > 
> > > > 
> > > > Sincerely,
> > > > Jonathan
> > > > 
> > > > On Fri, Sep 1, 2017 at 4:49 PM, Wolfgang Jeltsch
> > > > <wolfgang-it at jeltsch.info> wrote:
> > > > > 
> > > > > 
> > > > > 
> > > > > Hi!
> > > > > 
> > > > > Both the sliding law and the nesting law seem to make sense
> > > > > for
> > > > > FunctorFix. The other two laws seem to fundamentally rely on
> > > > > the
> > > > > existence of return (purity law) and (>>=) (left-shrinking).
> > > > > 
> > > > > However, there is also the scope change law, mentioned on page
> > > > > 19 of
> > > > > Levent Erkok’s thesis (http://digitalcommons.ohsu.edu/etd/164/
> > > > > ).
> > > > > This
> > > > > law can be formulated based on fmap, without resorting to
> > > > > return
> > > > > and
> > > > > (>>=). Levent proves it using all four MonadFix axioms. I do
> > > > > not
> > > > > know
> > > > > whether it is possible to derive it just from sliding,
> > > > > nesting,
> > > > > and
> > > > > the
> > > > > Functor laws, or whether we would need to require it
> > > > > explicitly.
> > > > > 
> > > > > Every type that is an instance of MonadFix, should be an
> > > > > instance of
> > > > > FunctorFix, with ffix being the same as mfix. At the moment, I
> > > > > cannot
> > > > > come up with a FunctorFix instance that is not an instance of
> > > > > Monad.
> > > > > 
> > > > > My desire for FunctorFix comes from my work on the new version
> > > > > of
> > > > > the
> > > > > incremental-computing package. In this package, I have certain
> > > > > operations that were supposed to work for all functors. I
> > > > > found
> > > > > out
> > > > > that
> > > > > I need these functors to have mfix-like operations, but I do
> > > > > not
> > > > > want to
> > > > > impose a Monad constraint on them, because I do not need
> > > > > return
> > > > > or
> > > > > (>>=).
> > > > > 
> > > > > All the best,
> > > > > Wolfgang
> > > > > 
> > > > > Am Mittwoch, den 30.08.2017, 16:30 -0400 schrieb David Feuer:
> > > > > > 
> > > > > > 
> > > > > > 
> > > > > > 
> > > > > > I assume you want to impose the MonadFix sliding law,
> > > > > > 
> > > > > > ffix (fmap h . f) = fmap h (ffix (f . h)), for strict h.
> > > > > > 
> > > > > > 
> > > > > > Do you also want the nesting law?
> > > > > > 
> > > > > > ffix (\x -> ffix (\y -> f x y)) = ffix (\x -> f x x)
> > > > > > 
> > > > > > Are there any other laws you'd like to add in place of the
> > > > > > seemingly
> > > > > > irrelevant purity and left shrinking laws?
> > > > > > 
> > > > > > Can you give some sample instances and how one might use
> > > > > > them?
> > > > > > 
> > > > > > On Wed, Aug 30, 2017 at 2:59 PM, Wolfgang Jeltsch
> > > > > > <wolfgang-it at jeltsch.info> wrote:
> > > > > > > 
> > > > > > > 
> > > > > > > 
> > > > > > > 
> > > > > > > 
> > > > > > > Hi!
> > > > > > > 
> > > > > > > There is the MonadFix class with the mfix method. However,
> > > > > > > there
> > > > > > > are
> > > > > > > situations where you need a fixed point operator of type a
> > > > > > > -> f
> > > > > > > a
> > > > > > > for
> > > > > > > some f, but f is not necessarily a monad. What about
> > > > > > > adding
> > > > > > > a
> > > > > > > FunctorFix
> > > > > > > class that is identical to MonadFix, except that it has a
> > > > > > > Functor,
> > > > > > > not a
> > > > > > > Monad, superclass constraint?
> > > > > > > 
> > > > > > > All the best,
> > > > > > > Wolfgang
> > > > > > > _______________________________________________
> > > > > > > Libraries mailing list
> > > > > > > Libraries at haskell.org
> > > > > > > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> > > > > _______________________________________________
> > > > > Libraries mailing list
> > > > > Libraries at haskell.org
> > > > > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> > > _______________________________________________
> > > Libraries mailing list
> > > Libraries at haskell.org
> > > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries