FunctorFix

[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