FunctorFix

[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