FunctorFix

[Wolfgang Jeltsch]

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