<div dir="auto"><div>Is it possible to implement a law-abiding (or useful) unapply for IO? That's a practically important MonadFix instance.</div><div dir="auto"><div class="gmail_extra" dir="auto"><br><div class="gmail_quote">On Sep 6, 2017 12:42 AM, "Jonathan S" <<a href="mailto:gereeter%2Bhaskell.libraries@gmail.com">gereeter+haskell.libraries@gmail.com</a>> wrote:<br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I've structured this email with a bunch of sections because it is a<br>
bit overly long.<br>
<br>
# A replacement for `FunctorFix`<br>
After thinking about this problem a bit more, I'm actually thinking<br>
that we might want a slightly stronger class (bikeshedding is<br>
welcome):<br>
<br>
class Functor f => Unapply f where<br>
    -- | This has a single law:<br>
    -- > fmap (\g -> g x) (unapply f) == f x<br>
    unapply :: (a -> f b) -> f (a -> b)<br>
<br>
ffix :: Unapply f => (a -> f a) -> f a<br>
ffix = fmap fix . unapply<br>
<br>
For efficiency, we'd probably want to add more methods to the class;<br>
I'll get back to that.<br>
<br>
The semantics of unapply is to take a function that produces a<br>
container of some fixed "shape" and fill that shape with functions<br>
that extract the result at the given position. Since that isn't a<br>
clear description at all,<br>
<br>
unapply (\x -> [f x, g x]) == [f, g]<br>
<br>
The implementations of this class follow the same general pattern. The<br>
input function is evaluated at bottom to figure out the correct shape,<br>
and then that shape is filled with copies of the input function<br>
composed with projection functions. For example:<br>
<br>
instance Unapply [] where<br>
    unapply f = case f (error "Strict function passed to unapply") of<br>
        [] -> []<br>
        (_:_) -> head . f : unapply (tail . f)<br>
<br>
Notably, while the only interesting new instance I figured out for<br>
FunctorFix was for the sum of functors (:+:), I couldn't figure out a<br>
way to implement FunctorFix for the composition of two functors (:.:).<br>
Unapply, however, clearly is closed under functor composition:<br>
<br>
instance (Unapply f, Unapply g) => Unapply (f :.: g) where<br>
    unapply f = Comp1 (fmap unapply (unapply (unComp1 . f)))<br>
<br>
# Proofs<br>
Now, this simple function with its one law is enough to derive *all*<br>
the laws we want for ffix (or even afix or mfix), using the fact that<br>
<br>
forall x. fmap (\g -> g x) u = fmap (\g -> g x) v<br>
<br>
implies u = v (up to the existance of `seq`, that is; I think things<br>
still work out with `seq` in the picture, but they get a lot messier).<br>
<br>
## Lemmas<br>
### Left lemma<br>
Forall x,<br>
fmap (\g -> g x) (unapply (fmap h . f))<br>
= {constant application}<br>
fmap h (f x)<br>
= {constant application}<br>
fmap h (fmap (\g -> g x) (unapply f))<br>
=<br>
fmap (\g -> h (g x)) (unapply f)<br>
=<br>
fmap (\g' -> g' x) (fmap (h .) (unapply f))<br>
Therefore,<br>
unapply (fmap h . f) = fmap (h .) (unapply f)<br>
<br>
### Right lemma<br>
Forall x,<br>
fmap (\g -> g x) (unapply (f . h))<br>
= {constant application}<br>
f (h x)<br>
= {constant application}<br>
fmap (\g -> g (h x)) (unapply f)<br>
=<br>
fmap (\g' -> g' x) (fmap (. h) (unapply f))<br>
Therefore,<br>
unapply (f . h) = fmap (. h) (unapply f)<br>
<br>
### Nesting lemma<br>
Forall x,<br>
fmap (\g' -> g' x) (fmap (\g y -> g y y) (unapply (unapply . f)))<br>
=<br>
fmap (\g -> g x x) (unapply (unapply . f))<br>
=<br>
fmap (\g' -> g' x) (fmap (\g -> g x) (unapply (unapply . f)))<br>
= {constant application}<br>
fmap (\g' -> g' x) (unapply (f x))<br>
= {constant application}<br>
f x x<br>
=<br>
(\y -> f y y) x<br>
= {constant application}<br>
fmap (\g -> g x) (unapply (\y -> f y y))<br>
Therefore,<br>
fmap (\g y -> g y y) (unapply (unapply . f)) = unapply (\y -> f y y)<br>
<br>
### Inner application lemma<br>
Forall f,<br>
fmap (\g' -> g' f) (unapply (\g -> fmap g u))<br>
= {constant application}<br>
fmap f u<br>
=<br>
fmap (\applyx -> applyx f) (fmap (\x g -> g x) u)<br>
Therefore,<br>
unapply (\g -> fmap g u) = fmap (\x g -> g x) u<br>
<br>
### Join lemma<br>
Forall x,<br>
fmap (\g -> g x) (join (fmap unapply (unapply f)))<br>
=<br>
join (fmap (fmap (\g -> g x)) (fmap unapply (unapply f)))<br>
=<br>
join (fmap (\h -> fmap (\g -> g x) (unapply h)) (unapply f))<br>
= {constant application}<br>
join (fmap (\h -> h x) (unapply f))<br>
= {constant application}<br>
join (f x)<br>
= {constant application}<br>
fmap (\g -> g x) (unapply (join . f))<br>
Therefore,<br>
join (fmap unapply (unapply f)) = unapply (join . f)<br>
<br>
## Strictness<br>
f ⊥ = ⊥<br>
⇔ {constant application}<br>
fmap (\g -> g x) (unapply f) = ⊥<br>
⇔ {strictness of `fmap`}<br>
unapply f = ⊥<br>
⇔ {strictness of `fmap`}<br>
fmap fix (unapply f) = ⊥<br>
⇔ {definition of `ffix`}<br>
ffix f = ⊥<br>
<br>
## Sliding<br>
<div class="quoted-text">ffix (fmap h . f)<br>
</div>= {definition of `ffix`}<br>
fmap fix (unapply (fmap h . f))<br>
= {left lemma}<br>
fmap fix (fmap (h .) (unapply f))<br>
=<br>
fmap (\g -> fix (h . g)) (unapply f)<br>
= {sliding (`fix`)}<br>
fmap (\g -> h (fix (g . h))) (unapply f)<br>
=<br>
fmap h (fmap fix (fmap (. h) (unapply f)))<br>
= {right lemma}<br>
fmap h (fmap fix (unapply (f . h)))<br>
= {definition of `ffix`}<br>
<div class="quoted-text">fmap h (ffix (f . h))<br>
<br>
</div>## Nesting<br>
<div class="quoted-text">ffix (\x -> ffix (\y -> f x y))<br>
</div>= {definition of `ffix`}<br>
fmap fix (unapply (\x -> fmap fix (unapply (\y -> f x y))))<br>
=<br>
fmap fix (unapply (fmap fix . unapply . f))<br>
= {left lemma}<br>
fmap fix (fmap (fix .) (unapply (unapply . f)))<br>
=<br>
fmap (\g -> fix (\x -> fix (\y -> g x y))) (unapply (unapply . f))<br>
= {nesting (`fix`)}<br>
fmap (\g -> fix (\x -> g x x)) (unapply (unapply . f))<br>
=<br>
fmap fix (fmap (\g x -> g x x) (unapply (unapply . f)))<br>
= {nesting lemma}<br>
fmap fix (unapply (\x -> f x x))<br>
= {definition of `ffix`}<br>
<div class="quoted-text">ffix (\x -> f x x)<br>
<br>
</div>## Pure left shrinking<br>
ffix (\x -> fmap (f x) u)<br>
= {definition of `ffix`}<br>
fmap fix (unapply (\x -> fmap (f x) u))<br>
=<br>
fmap fix (unapply ((\g -> fmap g u) . f))<br>
= {right lemma}<br>
fmap fix (fmap (. f) (unapply (\g -> fmap g u)))<br>
= {inner application lemma}<br>
fmap fix (fmap (. f) (fmap (\y g -> g y) u))<br>
<div class="quoted-text">=<br>
fmap (\y -> fix (\x -> f x y))<br>
<br>
</div>## Left shrinking<br>
ffix (\x -> a >>= \y -> f x y)<br>
= {definition of `ffix`}<br>
fmap fix (unapply (\x -> a >>= \y -> f x y))<br>
=<br>
fmap fix (unapply ((a >>=) . f))<br>
= {right lemma}<br>
fmap fix (fmap (. f) (unapply (\g -> a >>= g)))<br>
=<br>
fmap fix (fmap (. f) (unapply (join . (\g -> fmap g a))))<br>
= {join lemma}<br>
fmap fix (fmap (. f) (join (fmap unapply (unapply (\g -> fmap g a)))))<br>
= {inner application lemma}<br>
fmap fix (fmap (. f) (join (fmap unapply (fmap (\y g -> g y) a))))<br>
=<br>
join (fmap (fmap fix . fmap (. f) . unapply . (\y g -> g y)) a)<br>
=<br>
a >>= \y -> fmap fix (fmap (. f) (unapply (\g -> g y)))<br>
= {right lemma}<br>
a >>= \y -> fmap fix (unapply ((\g -> g y) . f))<br>
=<br>
a >>= \y -> fmap fix (unapply (\x -> f x y))<br>
= {definition of `ffix`}<br>
a >>= \y -> ffix (\x -> f x y)<br>
<br>
# Efficiency<br>
I should preface this section by saying that I haven't actually done<br>
any benchmarking or profiling.<br>
<br>
Unfortunately, the Unapply solution seems to be slightly slower than<br>
directly implementing FunctorFix, for two reasons. First, with<br>
Unapply, the call to ffix is split into two pieces, first constructing<br>
the resultant data structure and then mapping over that to calculate<br>
fixed points. Especially since unapply may be recursive and might not<br>
be inlined, this can result in intermediate data structures and<br>
slowness. This is easily fixed. Instead of implementing unapply<br>
directly, we can add a new method to the class,<br>
<br>
unapplyMap :: ((a -> b) -> c) -> (a -> f b) -> f c<br>
<br>
defined by<br>
<br>
unapplyMap f = fmap f . unapply<br>
unapply = unapplyMap id<br>
<br>
Finally, we just implement unapplyMap directly instead of using<br>
unapply and use unapplyMap in the definition of ffix.<br>
<br>
The second performance problem is more subtle. It comes from the fact<br>
that the current implementation of mfix for sum types is *speculative*<br>
in a sense. While the Unapply instance for [] given above is perfectly<br>
valid, it operates in two steps. In the first step, it calls f on<br>
bottom to determing whether the result is a cons node or nil, and in<br>
the second step, it extracts the appropriate components. The standard<br>
library implementation, in contrast, just initially assumes that f<br>
will return a cons node, calling `fix (head . f)`. If that results in<br>
[], it will back off and return [], but otherwise it can just extract<br>
the correct head immediately. To look at concrete instances, compare:<br>
<br>
-- Equation 4.3 in Erkok's thesis, unoptimized<br>
instance FunctorFix Maybe where<br>
    ffix f = case f (error "Strict function passed to ffix") of<br>
        Nothing -> Nothing<br>
        Just _ -> Just (fix (unJust . f))<br>
      where<br>
        unJust (Just x) = x<br>
<br>
-- Equation 4.2 in Erkok's thesis, optimized<br>
instance FunctorFix Maybe where<br>
    ffix f = fix (f . unJust)<br>
      where<br>
        unJust (Just x) = x<br>
<br>
-- Reformulation of Equation 4.2 that shows the equivalence of the two<br>
approaches<br>
instance FunctorFix Maybe where<br>
    ffix f = case f (fix (unJust . f)) {- = fix (f . unJust) -} of<br>
        Nothing -> Nothing<br>
        Just x -> Just (x {- = unJust (f (fix (unJust . f))) = fix<br>
(unJust . f) -})<br>
<br>
Essentially, the optimized implementation is still passing something<br>
to f and checking the result, but it chooses what to pass to f in a<br>
clever way so that, in the Just case, it can be reused.<br>
<br>
This optimization is nice and useful, but it isn't composable. Even<br>
though it follows the same pattern of implementation, I don't see a<br>
way to directly use this optimization in the implementation for (:+:).<br>
It curcially relies on repliacing `fix (project . f)` with `fix (f .<br>
project)`, and the latter simply does not typecheck when `project`<br>
does not return a single value.<br>
<br>
I don't see any good way to integrate this optimization into Unapply.<br>
To do so we'd need to know about the feedback inherent in a fixpoint<br>
to know to pass something useful into f when figuring out the shape of<br>
the result. The simplest solution would be to keep ffix in the type<br>
class and implement it independently of unapply whenever possible<br>
(a.k.a. everywhere but in the instance for (:.:)), but that seems ugly<br>
to me.<br>
<div class="elided-text"><br>
On Tue, Sep 5, 2017 at 6:35 PM, David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br>
> As long as we're going down this path, we should also consider<br>
> ApplicativeFix. All the laws except left shrinking make immediate<br>
> sense in that context. That surely has a law or two of its own. For<br>
> example, I'd expect that<br>
><br>
> afix (\x -> a *> f x) = a *> afix f<br>
><br>
> I don't know if it has anything more interesting.<br>
><br>
><br>
> On Tue, Sep 5, 2017 at 6:11 PM, Wolfgang Jeltsch<br>
> <<a href="mailto:wolfgang-it@jeltsch.info">wolfgang-it@jeltsch.info</a>> wrote:<br>
>> Jonathan, thanks a lot for working this out. Impressive!<br>
>><br>
>> So we want the following laws for FunctorFix:<br>
>><br>
>> Pure left shrinking:<br>
>><br>
>>     ffix (\x -> fmap (f x) g) = fmap (\y -> fix (\x -> f x y)) g<br>
>><br>
>> Sliding:<br>
>><br>
>>     ffix (fmap h . f) = fmap h (ffix (f . h))<br>
>><br>
>>     for strict h<br>
>><br>
>> Nesting:<br>
>><br>
>>     ffix (\x -> ffix (\y -> f x y)) = ffix (\x -> f x x)<br>
>><br>
>> Levent Erkok’s thesis also mentions a strictness law for monadic fixed<br>
>> points, which is not mentioned in the documentation of<br>
>> Control.Monad.Fix. It goes as follows:<br>
>><br>
>> Strictness:<br>
>><br>
>>     f ⊥ = ⊥ ⇔ mfix f = ⊥<br>
>><br>
>> Does this hold automatically, or did the designers of Control.Monad.Fix<br>
>> considered it inappropriate to require this?<br>
>><br>
>> All the best,<br>
>> Wolfgang<br>
>><br>
>> Am Samstag, den 02.09.2017, 14:08 -0500 schrieb Jonathan S:<br>
>>> I think that in addition to nesting and sliding, we should have the<br>
>>> following law:<br>
>>><br>
>>> ffix (\x -> fmap (f x) g) = fmap (\y -> fix (\x -> f x y)) g<br>
>>><br>
>>> I guess I'd call this the "pure left shrinking" law because it is the<br>
>>> composition of left shrinking and purity:<br>
>>><br>
>>> ffix (\x -> fmap (f x) g)<br>
>>> =<br>
>>> ffix (\x -> g >>= \y -> return (f x y))<br>
>>> = {left shrinking}<br>
>>> g >>= \y -> ffix (\x -> return (f x y))<br>
>>> = {purity}<br>
>>> g >>= \y -> return (fix (\x -> f x y))<br>
>>> =<br>
>>> fmap (\y -> fix (\x -> f x y)) g<br>
>>><br>
>>> This is powerful enough to prove the scope change law, but is<br>
>>> significantly simpler:<br>
>>><br>
>>> ffix (\~(a, b) -> fmap (\a' -> (a', h a' a b)) (f a))<br>
>>> =<br>
>>> ffix (\t -> fmap (\a' -> (a', h a' (fst t) (snd t))) (f (fst t)))<br>
>>> = {nesting}<br>
>>> ffix (\t1 -> ffix (\t2 -> fmap (\a' -> (a', h a' (fst t1) (snd t1)))<br>
>>> (f (fst t2))))<br>
>>> =<br>
>>> ffix (\~(a, b) -> ffix (fmap (\a' -> (a', h a' a b)) . f . fst))<br>
>>> = {sliding}<br>
>>> ffix (\~(a, b) -> fmap (\a' -> (a', h a' a b)) (ffix (f . fst . (\a'<br>
>>> -> (a', h a' a b)))))<br>
>>> =<br>
>>> ffix (\~(a, b) -> fmap (\a' -> (a', h a' a b)) (ffix f))<br>
>>> = {pure left shrinking}<br>
>>> fmap (\a' -> fix (\~(a, b) -> (a', h a' a b))) (ffix f)<br>
>>><br>
>>> Moreover, it seems necessary to prove that ffix interacts well with<br>
>>> constant functions:<br>
>>><br>
>>> ffix (const a)<br>
>>> =<br>
>>> ffix (\_ -> fmap id a)<br>
>>> =<br>
>>> fmap (\y -> fix (\_ -> id y)) a<br>
>>> =<br>
>>> fmap id a<br>
>>> =<br>
>>> a<br>
>>><br>
>>> In addition, when the functor in question is in fact a monad, it<br>
>>> implies purity:<br>
>>><br>
>>> ffix (return . f)<br>
>>> =<br>
>>> ffix (\x -> return (f x))<br>
>>> =<br>
>>> ffix (\x -> fmap (\_ -> f x) (return ()))<br>
>>> =<br>
>>> fmap (\_ -> fix (\x -> f x)) (return ())<br>
>>> =<br>
>>> return (fix f)<br>
>>><br>
>>><br>
>>> Sincerely,<br>
>>> Jonathan<br>
>>><br>
>>> On Fri, Sep 1, 2017 at 4:49 PM, Wolfgang Jeltsch<br>
>>> <<a href="mailto:wolfgang-it@jeltsch.info">wolfgang-it@jeltsch.info</a>> wrote:<br>
>>> ><br>
>>> > Hi!<br>
>>> ><br>
>>> > Both the sliding law and the nesting law seem to make sense for<br>
>>> > FunctorFix. The other two laws seem to fundamentally rely on the<br>
>>> > existence of return (purity law) and (>>=) (left-shrinking).<br>
>>> ><br>
>>> > However, there is also the scope change law, mentioned on page 19 of<br>
>>> > Levent Erkok’s thesis (<a href="http://digitalcommons.ohsu.edu/etd/164/" rel="noreferrer" target="_blank">http://digitalcommons.ohsu.<wbr>edu/etd/164/</a>).<br>
>>> > This<br>
>>> > law can be formulated based on fmap, without resorting to return and<br>
>>> > (>>=). Levent proves it using all four MonadFix axioms. I do not<br>
>>> > know<br>
>>> > whether it is possible to derive it just from sliding, nesting, and<br>
>>> > the<br>
>>> > Functor laws, or whether we would need to require it explicitly.<br>
>>> ><br>
>>> > Every type that is an instance of MonadFix, should be an instance of<br>
>>> > FunctorFix, with ffix being the same as mfix. At the moment, I<br>
>>> > cannot<br>
>>> > come up with a FunctorFix instance that is not an instance of Monad.<br>
>>> ><br>
>>> > My desire for FunctorFix comes from my work on the new version of<br>
>>> > the<br>
>>> > incremental-computing package. In this package, I have certain<br>
>>> > operations that were supposed to work for all functors. I found out<br>
>>> > that<br>
>>> > I need these functors to have mfix-like operations, but I do not<br>
>>> > want to<br>
>>> > impose a Monad constraint on them, because I do not need return or<br>
>>> > (>>=).<br>
>>> ><br>
>>> > All the best,<br>
>>> > Wolfgang<br>
>>> ><br>
>>> > Am Mittwoch, den 30.08.2017, 16:30 -0400 schrieb David Feuer:<br>
>>> > ><br>
>>> > ><br>
>>> > > I assume you want to impose the MonadFix sliding law,<br>
>>> > ><br>
>>> > > ffix (fmap h . f) = fmap h (ffix (f . h)), for strict h.<br>
>>> > ><br>
>>> > ><br>
>>> > > Do you also want the nesting law?<br>
>>> > ><br>
>>> > > ffix (\x -> ffix (\y -> f x y)) = ffix (\x -> f x x)<br>
>>> > ><br>
>>> > > Are there any other laws you'd like to add in place of the<br>
>>> > > seemingly<br>
>>> > > irrelevant purity and left shrinking laws?<br>
>>> > ><br>
>>> > > Can you give some sample instances and how one might use them?<br>
>>> > ><br>
>>> > > On Wed, Aug 30, 2017 at 2:59 PM, Wolfgang Jeltsch<br>
>>> > > <<a href="mailto:wolfgang-it@jeltsch.info">wolfgang-it@jeltsch.info</a>> wrote:<br>
>>> > > ><br>
>>> > > ><br>
>>> > > ><br>
>>> > > > Hi!<br>
>>> > > ><br>
>>> > > > There is the MonadFix class with the mfix method. However, there<br>
>>> > > > are<br>
>>> > > > situations where you need a fixed point operator of type a -> f<br>
>>> > > > a<br>
>>> > > > for<br>
>>> > > > some f, but f is not necessarily a monad. What about adding a<br>
>>> > > > FunctorFix<br>
>>> > > > class that is identical to MonadFix, except that it has a<br>
>>> > > > Functor,<br>
>>> > > > not a<br>
>>> > > > Monad, superclass constraint?<br>
>>> > > ><br>
>>> > > > All the best,<br>
>>> > > > Wolfgang<br>
>>> > > > ______________________________<wbr>_________________<br>
>>> > > > Libraries mailing list<br>
>>> > > > <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
>>> > > > <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><br>
>>> > ______________________________<wbr>_________________<br>
>>> > Libraries mailing list<br>
>>> > <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
>>> > <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><br>
>> ______________________________<wbr>_________________<br>
>> Libraries mailing list<br>
>> <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><br>
> ______________________________<wbr>_________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><br>
</div></blockquote></div><br></div></div></div>