FunctorFix

[Chris Wong]

Your Unapply class looks a bit like Distributive, but with f ~ ((->) r).

I wonder if there's a connection there?

https://hackage.haskell.org/package/distributive-0.5.3/docs/Data-Distributive.html

On Wed, Sep 6, 2017 at 4:42 PM, Jonathan S <
gereeter+haskell.libraries at gmail.com> wrote:

> I've structured this email with a bunch of sections because it is a
> bit overly long.
>
> # A replacement for `FunctorFix`
> After thinking about this problem a bit more, I'm actually thinking
> that we might want a slightly stronger class (bikeshedding is
> welcome):
>
> class Functor f => Unapply f where
>     -- | This has a single law:
>     -- > fmap (\g -> g x) (unapply f) == f x
>     unapply :: (a -> f b) -> f (a -> b)
>
> ffix :: Unapply f => (a -> f a) -> f a
> ffix = fmap fix . unapply
>
> For efficiency, we'd probably want to add more methods to the class;
> I'll get back to that.
>
> The semantics of unapply is to take a function that produces a
> container of some fixed "shape" and fill that shape with functions
> that extract the result at the given position. Since that isn't a
> clear description at all,
>
> unapply (\x -> [f x, g x]) == [f, g]
>
> The implementations of this class follow the same general pattern. The
> input function is evaluated at bottom to figure out the correct shape,
> and then that shape is filled with copies of the input function
> composed with projection functions. For example:
>
> instance Unapply [] where
>     unapply f = case f (error "Strict function passed to unapply") of
>         [] -> []
>         (_:_) -> head . f : unapply (tail . f)
>
> Notably, while the only interesting new instance I figured out for
> FunctorFix was for the sum of functors (:+:), I couldn't figure out a
> way to implement FunctorFix for the composition of two functors (:.:).
> Unapply, however, clearly is closed under functor composition:
>
> instance (Unapply f, Unapply g) => Unapply (f :.: g) where
>     unapply f = Comp1 (fmap unapply (unapply (unComp1 . f)))
>
> # Proofs
> Now, this simple function with its one law is enough to derive *all*
> the laws we want for ffix (or even afix or mfix), using the fact that
>
> forall x. fmap (\g -> g x) u = fmap (\g -> g x) v
>
> implies u = v (up to the existance of `seq`, that is; I think things
> still work out with `seq` in the picture, but they get a lot messier).
>
> ## Lemmas
> ### Left lemma
> Forall x,
> fmap (\g -> g x) (unapply (fmap h . f))
> = {constant application}
> fmap h (f x)
> = {constant application}
> fmap h (fmap (\g -> g x) (unapply f))
> =
> fmap (\g -> h (g x)) (unapply f)
> =
> fmap (\g' -> g' x) (fmap (h .) (unapply f))
> Therefore,
> unapply (fmap h . f) = fmap (h .) (unapply f)
>
> ### Right lemma
> Forall x,
> fmap (\g -> g x) (unapply (f . h))
> = {constant application}
> f (h x)
> = {constant application}
> fmap (\g -> g (h x)) (unapply f)
> =
> fmap (\g' -> g' x) (fmap (. h) (unapply f))
> Therefore,
> unapply (f . h) = fmap (. h) (unapply f)
>
> ### Nesting lemma
> Forall x,
> fmap (\g' -> g' x) (fmap (\g y -> g y y) (unapply (unapply . f)))
> =
> fmap (\g -> g x x) (unapply (unapply . f))
> =
> fmap (\g' -> g' x) (fmap (\g -> g x) (unapply (unapply . f)))
> = {constant application}
> fmap (\g' -> g' x) (unapply (f x))
> = {constant application}
> f x x
> =
> (\y -> f y y) x
> = {constant application}
> fmap (\g -> g x) (unapply (\y -> f y y))
> Therefore,
> fmap (\g y -> g y y) (unapply (unapply . f)) = unapply (\y -> f y y)
>
> ### Inner application lemma
> Forall f,
> fmap (\g' -> g' f) (unapply (\g -> fmap g u))
> = {constant application}
> fmap f u
> =
> fmap (\applyx -> applyx f) (fmap (\x g -> g x) u)
> Therefore,
> unapply (\g -> fmap g u) = fmap (\x g -> g x) u
>
> ### Join lemma
> Forall x,
> fmap (\g -> g x) (join (fmap unapply (unapply f)))
> =
> join (fmap (fmap (\g -> g x)) (fmap unapply (unapply f)))
> =
> join (fmap (\h -> fmap (\g -> g x) (unapply h)) (unapply f))
> = {constant application}
> join (fmap (\h -> h x) (unapply f))
> = {constant application}
> join (f x)
> = {constant application}
> fmap (\g -> g x) (unapply (join . f))
> Therefore,
> join (fmap unapply (unapply f)) = unapply (join . f)
>
> ## Strictness
> f ⊥ = ⊥
> ⇔ {constant application}
> fmap (\g -> g x) (unapply f) = ⊥
> ⇔ {strictness of `fmap`}
> unapply f = ⊥
> ⇔ {strictness of `fmap`}
> fmap fix (unapply f) = ⊥
> ⇔ {definition of `ffix`}
> ffix f = ⊥
>
> ## Sliding
> ffix (fmap h . f)
> = {definition of `ffix`}
> fmap fix (unapply (fmap h . f))
> = {left lemma}
> fmap fix (fmap (h .) (unapply f))
> =
> fmap (\g -> fix (h . g)) (unapply f)
> = {sliding (`fix`)}
> fmap (\g -> h (fix (g . h))) (unapply f)
> =
> fmap h (fmap fix (fmap (. h) (unapply f)))
> = {right lemma}
> fmap h (fmap fix (unapply (f . h)))
> = {definition of `ffix`}
> fmap h (ffix (f . h))
>
> ## Nesting
> ffix (\x -> ffix (\y -> f x y))
> = {definition of `ffix`}
> fmap fix (unapply (\x -> fmap fix (unapply (\y -> f x y))))
> =
> fmap fix (unapply (fmap fix . unapply . f))
> = {left lemma}
> fmap fix (fmap (fix .) (unapply (unapply . f)))
> =
> fmap (\g -> fix (\x -> fix (\y -> g x y))) (unapply (unapply . f))
> = {nesting (`fix`)}
> fmap (\g -> fix (\x -> g x x)) (unapply (unapply . f))
> =
> fmap fix (fmap (\g x -> g x x) (unapply (unapply . f)))
> = {nesting lemma}
> fmap fix (unapply (\x -> f x x))
> = {definition of `ffix`}
> ffix (\x -> f x x)
>
> ## Pure left shrinking
> ffix (\x -> fmap (f x) u)
> = {definition of `ffix`}
> fmap fix (unapply (\x -> fmap (f x) u))
> =
> fmap fix (unapply ((\g -> fmap g u) . f))
> = {right lemma}
> fmap fix (fmap (. f) (unapply (\g -> fmap g u)))
> = {inner application lemma}
> fmap fix (fmap (. f) (fmap (\y g -> g y) u))
> =
> fmap (\y -> fix (\x -> f x y))
>
> ## Left shrinking
> ffix (\x -> a >>= \y -> f x y)
> = {definition of `ffix`}
> fmap fix (unapply (\x -> a >>= \y -> f x y))
> =
> fmap fix (unapply ((a >>=) . f))
> = {right lemma}
> fmap fix (fmap (. f) (unapply (\g -> a >>= g)))
> =
> fmap fix (fmap (. f) (unapply (join . (\g -> fmap g a))))
> = {join lemma}
> fmap fix (fmap (. f) (join (fmap unapply (unapply (\g -> fmap g a)))))
> = {inner application lemma}
> fmap fix (fmap (. f) (join (fmap unapply (fmap (\y g -> g y) a))))
> =
> join (fmap (fmap fix . fmap (. f) . unapply . (\y g -> g y)) a)
> =
> a >>= \y -> fmap fix (fmap (. f) (unapply (\g -> g y)))
> = {right lemma}
> a >>= \y -> fmap fix (unapply ((\g -> g y) . f))
> =
> a >>= \y -> fmap fix (unapply (\x -> f x y))
> = {definition of `ffix`}
> a >>= \y -> ffix (\x -> f x y)
>
> # Efficiency
> I should preface this section by saying that I haven't actually done
> any benchmarking or profiling.
>
> Unfortunately, the Unapply solution seems to be slightly slower than
> directly implementing FunctorFix, for two reasons. First, with
> Unapply, the call to ffix is split into two pieces, first constructing
> the resultant data structure and then mapping over that to calculate
> fixed points. Especially since unapply may be recursive and might not
> be inlined, this can result in intermediate data structures and
> slowness. This is easily fixed. Instead of implementing unapply
> directly, we can add a new method to the class,
>
> unapplyMap :: ((a -> b) -> c) -> (a -> f b) -> f c
>
> defined by
>
> unapplyMap f = fmap f . unapply
> unapply = unapplyMap id
>
> Finally, we just implement unapplyMap directly instead of using
> unapply and use unapplyMap in the definition of ffix.
>
> The second performance problem is more subtle. It comes from the fact
> that the current implementation of mfix for sum types is *speculative*
> in a sense. While the Unapply instance for [] given above is perfectly
> valid, it operates in two steps. In the first step, it calls f on
> bottom to determing whether the result is a cons node or nil, and in
> the second step, it extracts the appropriate components. The standard
> library implementation, in contrast, just initially assumes that f
> will return a cons node, calling `fix (head . f)`. If that results in
> [], it will back off and return [], but otherwise it can just extract
> the correct head immediately. To look at concrete instances, compare:
>
> -- Equation 4.3 in Erkok's thesis, unoptimized
> instance FunctorFix Maybe where
>     ffix f = case f (error "Strict function passed to ffix") of
>         Nothing -> Nothing
>         Just _ -> Just (fix (unJust . f))
>       where
>         unJust (Just x) = x
>
> -- Equation 4.2 in Erkok's thesis, optimized
> instance FunctorFix Maybe where
>     ffix f = fix (f . unJust)
>       where
>         unJust (Just x) = x
>
> -- Reformulation of Equation 4.2 that shows the equivalence of the two
> approaches
> instance FunctorFix Maybe where
>     ffix f = case f (fix (unJust . f)) {- = fix (f . unJust) -} of
>         Nothing -> Nothing
>         Just x -> Just (x {- = unJust (f (fix (unJust . f))) = fix
> (unJust . f) -})
>
> Essentially, the optimized implementation is still passing something
> to f and checking the result, but it chooses what to pass to f in a
> clever way so that, in the Just case, it can be reused.
>
> This optimization is nice and useful, but it isn't composable. Even
> though it follows the same pattern of implementation, I don't see a
> way to directly use this optimization in the implementation for (:+:).
> It curcially relies on repliacing `fix (project . f)` with `fix (f .
> project)`, and the latter simply does not typecheck when `project`
> does not return a single value.
>
> I don't see any good way to integrate this optimization into Unapply.
> To do so we'd need to know about the feedback inherent in a fixpoint
> to know to pass something useful into f when figuring out the shape of
> the result. The simplest solution would be to keep ffix in the type
> class and implement it independently of unapply whenever possible
> (a.k.a. everywhere but in the instance for (:.:)), but that seems ugly
> to me.
>
> On Tue, Sep 5, 2017 at 6:35 PM, David Feuer <david.feuer at gmail.com> wrote:
> > 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
> > _______________________________________________
> > 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
>



-- 
Chris Wong (https://lambda.xyz)

"I had not the vaguest idea what this meant and when I could not remember
the words, my tutor threw the book at my head, which did not stimulate my
intellect in any way." -- Bertrand Russell
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170909/bd3d38aa/attachment-0001.html>