I can’t see how it could be done, since Lens law are about one lens but here we have two. And anyway Lens laws are about Lens, but here we have two getters. And in Getter’s doc we read:
Since a Getter cannot be used to write back there are no Lens laws that can be applied to it.
That’s why I think this should be provable without extra laws. Or should we add them to Getter’s doc? It’s very suspicious, if I’m the first one who recognized this.
type Getter s a = forall f. (Contravariant f, Functor f) => (a -> f a) -> s -> f s
which means when use use it as a Getting
type Getting r s a = (a -> Const r a) -> s -> Const r s
the r is parametric. Then you’ll get a free theorem that allows you to proceed with your proof above. I’m not sure what that free theorem is though. Parametricity always puzzles me.
That’s the spirit of it. If we have, for instance, a lens…
p :: forall f. Functor f => (a -> f b) -> (s -> f t)
… then f being parametric implies the following property, analogous to the naturality law of Traversable:
-- Given a natural transformation between Functors f and g:
-- t :: forall x. f x -> g x
p (t . k) = t . p k
In particular:
This property does rule out your counterexample: if p were to ignore its argument, we’d be left with t only on the right side of the equation above, which can’t hold in general, as we can encode arbitrary functions as natural transformations between Const functors.
@jaror 's property arises as a special case, with k = Const and f ~ g ~ Const a.
The property suffices to resume @Lev135’s derivation:
Thank’s. I’ve already proved this property by myself, but it seems that your argument is much more general is applicable to many other places, where I’d like to prove such things.
Does this hold for more restrictive constraints like (Functor f, Contravariant f)? How can it be proved? It’s important here, since I need to prove it for Getter’s here and in even more restrictive case.
I think “more restrictive” might be the wrong term, but if you mean by adding more constraints on the type of f, it doesn’t hold in general. If the constraints allows manufacturing an f t out of thin air, things can go wrong.
Consider
data T a = L | R
instance Functor T where
fmap _ L= L
fmap _ R = R
class IsoT f where
toT :: f a -> T a
fromT :: T a -> f a
instance IsoT T where
toT = id
fromT = id
-- and lets pick some values of p, t and k
p :: (Functor f, IsoT f) => (a -> f b) -> (s -> f t)
p _ _ = fromT R
t :: T x -> T x
t _ = L
k :: a -> T a
k _ = L
-- (t . p k) () = L
-- p (t . k) () = R
I don’t understand why it’s should be easier. If p knows about f more, it can do something with it so that it will not distribute in this manner, isn’t it?
Um, yes, I beg your pardon. I misunderstood what you meant by “more restrictive” (and then I failed to check your example).
Sure, you’re asking whether it works for (Functor f, Contravariant f) and I’m asking whether it works for Applicative f. Both are “more restrictive” on the type parameter f but less restrictive on the terms of the type
forall f. C f => (a -> f b) -> (s -> f t)
so they may not satisfy the desirable property.
I think the correct approach is to desugar the constraint into its dictionary and then obtain the free theorem a la Theorems for free!. So, for (Functor f, Contravariant f) the type in question would be
forall f. (Functor f, Covariant f) => (a -> f b) -> (s -> f t)
which desugars to
forall f a b s t.
(forall p q. (p -> q) -> f p -> f q) ->
(forall p q. (p -> q) -> f q -> f p) ->
(a -> f b) ->
(s -> f t)
But I’m not very good at deriving free theorems. Perhaps @duplode can help.
In general, we do have to be careful with additional constraints, as only natural transformations which preserve the extra class operations will be admissible. That’s why, for instance, the naturality law of Traversable only holds for natural transformations which preserve pure and (<*>). If we are only dealing with Functor and Contravariant, though, no restrictions are necessary, as parametricity on its own is enough to ensure fmap and contramap are preserved.
Indeed: the requirement that the class methods are preserved follows from that.