FunctorFix

[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