Re: FunctorFix

10 Sep 2017

      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
 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
 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
 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@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries