Is it possible to implement a law-abiding (or useful) unapply for IO?
That's a practically important MonadFix instance.
On Sep 6, 2017 12:42 AM, "Jonathan S" <gereeter+***@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.
Post by David FeuerAs 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
Post by Wolfgang JeltschJonathan, thanks a lot for working this out. Impressive!
ffix (\x -> fmap (f x) g) = fmap (\y -> fix (\x -> f x y)) g
ffix (fmap h . f) = fmap h (ffix (f . h))
for strict h
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
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
I think that in addition to nesting and sliding, we should have the
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
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
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
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
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
Post by Wolfgang JeltschHi!
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
Post by David FeuerI 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
Post by Wolfgang JeltschHi!
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries