1

Note: The current question is a follow-up to this one. It received a great answer by Daniel Wagner.

I am trying to figure out how to derive a natural map for the given type of kind * -> *. natmap is a natural map for F, if it is equal to:

To summarize, Daniel Wagner proposed an algorithm which derives fmap if the given functor is covariant or fails otherwise. The same could be done for contramap and invmap. They implemented fmap and contramap:

-- COVARIANT

fmap @(F + F') f (Left x) = Left (fmap @F f x)
fmap @(F + F') f (Right x) = Right (fmap @F' f x)
fmap @(F * F') f (x, y) = (fmap @F f x, fmap @F f y)
fmap @(Id) f x = f x
fmap @(Const X) f x = x
fmap @(F -> F') f x = fmap @F' f . x . contramap @F f

fmap @(F . F') f x = fmap @F (fmap @F' f) x
-- OR
fmap @(F . F') f x = contramap @F (contramap @F' f) x

-- CONTRAVARIANT

contramap @(F + F') f (Left x) = Left (contramap @F f x)
contramap @(F + F') f (Right x) = Right (contramap @F' f x)
contramap @(F * F') f (x, y) = (contramap @F f x, contramap @F' f y)
-- contramap @(Id) fails
contramap @(Const X) f x = x
contramap @(F -> F') f x = contramap @F' f . x . fmap @F f

contramap @(F . F') f x = contramap @F (fmap @F' f) x
-- OR
contramap @(F . F') f x = fmap @F (contramap @F' f) x

Daniel Wagner's answer got me thinking. It must be possible to substitute three algorithms (which derive fmap, contramap and invmap) with a single algorithm, which derives invmap. E. g.: we derived invmap for data F a = F (a, a) and while doing so figured out that F is covariant. Thus, we can define fmap f = invmap f undefined for F. And vice versa for data F' = F' ((a, a) -> Int): contramap g = invmap undefined g.

How Is invmap Derived?

Basically, we adjust Daniel Wagner's algorithm:

{- 1 -} invmap @(F + F') f g (Left x) = Left (invmap @F f g x)
{- 2 -} invmap @(F + F') f g (Right x) = Right (invmap @F' f g x)
{- 3 -} invmap @(F * F') f g (x, y) = (invmap @F f g x, invmap @F' f g y)
{- 4 -} invmap @(F -> F') f g x = invmap @F' f g . x . invmap @F g f

{- 5 -} invmap @(F . F') f g x = invmap @F (invmap @F' f g) (invmap @F' g f) x

{- 6 -} invmap @(Id) f g x = f x
{- 7 -} invmap @(Const X) f x = x

A few comments concerning some of the lines above:

5 The idea is that in invmap @F (invmap @F' a b) (invmap @F' c d):

  • a processes covariant positions in F which appear in covariant positions in F',
  • b processes contravariant positions in F which appear in covariant positions in F',
  • c processes covariant positions in F which appear in contravariant positions in F',
  • d processes contravariant positions in F which appear in contravariant positions in F'.

I. e. a and d process covariant positions, whereas b and c process contravariant positions. Thus, a = d = f; b = c = g.

6 Id leafcase indeed fails for contravariant functors as, when contramap g is called, undefined is put in f's place. Dually: Id leafcase is the only one to use f directly for covariant functors.

Why Does It Work?

I reckon this algorithm to work due to a simple reason: invmap does not actually have to use each of its arguments directly. Besides, when we try using the covaraint processor for a contravariant functor (i. e. running contramap @Id g x), we get an error (as the covariant processor is undefined).

Basically, I the idea came from implementing fmap and contramap in terms of invmap, just like phantom is implemented in terms of fmap and contramap.

Why Is It Interesting?

Branching produces some overheat. E. g.:

contramap @(F . F') f x = contramap @F (fmap @F' f) x
-- OR
contramap @(F . F') f x = fmap @F (contramap @F' f) x

Unless F and F' are phantom, one of the cases would have failed after examining the whole structure of F and F'. One may claim that choosing one out of two does not really classify as overheat and can be pardoned in order to maintain readability. But things get quite ugly with invmap. I consider there to be 7 subcases for each of the following cases: F -> F', F + F', F * F'. Such code seems to be quite inefficient.

All those subcases were generated by our assumptions concerning the variance. When we stop doing that deriving invmap only, the branching disappears.

The Question

Does this algorithm yield lawful natural maps? I don't think we can prove that fmap f = invmap f undefined for lawful instances. Rather, we depend on the fact that we run the contravariant processor iff we encounter a contravariant position (same for contravariant), which is the case in the algorithm above.

P. S. Some suggest the Invariant interface is inferior to Profunctors and should be avoided. But, if my algorithm is indeed correct, I think this is a pretty good use for such a class.

Zhiltsoff Igor
  • 1,812
  • 8
  • 24
  • 1
    I don't think your arrow case for `invmap` can be correct -- one or the other invocation of `invmap` on the RHS should have its arguments switched. – Daniel Wagner Jul 28 '21 at 20:16
  • @DanielWagner right, `F` is in the contravariant position, thus, the covariant processor shall deal with `F`'s contravariant positions and the contravariant - with `F`'s covariant positions. – Zhiltsoff Igor Jul 28 '21 at 20:20
  • What does "correct" mean in "is this solution correct"? For example, one thing you might mean is to ask whether it gives the same result(s) as the algorithm(s) in the previous answer. I guess another thing is to ask whether this algorithm yields `fmap`s and `contramap`s that satisfy the functor laws. And I guess there could be others, too? Anyway, I guess the answer to all of them is probably going to be: by induction on the structure of your functor. – Daniel Wagner Jul 28 '21 at 20:25
  • @DanielWagner Yes, I am looking for lawful instances. Don't the solutions from the previous answer yield lawful `fmap`s and `contramap`s? Besides, doesn't the `DeriveFunctor` extension, too (speaking of `fmap` only)? – Zhiltsoff Igor Jul 28 '21 at 20:30
  • I don't want to sound like a pest, but the question still isn't precise. Really, this is not quibbling, I promise -- figuring out what the heck you are trying to prove is usually 80% of the effort of making a proof, in my experience. So. You say "`natmap` is a natural map for `F`, if it matches: * `fmap` in case of covariant `F`" (and three other cases). What is `fmap`? How do you specify the thing we're trying to match? (...for that matter, what constitutes a match?) – Daniel Wagner Jul 28 '21 at 20:40
  • @DanielWagner I guess there are two ways: 1. `fmap` (**natural map**, speaking generally) is defined inductively by the rules in the linked answer; 2. `fmap` is a function which satisfies `Functor` laws. I guess those are complementary, but the second approach is more formal, so let’s choose the latter. As for the “match”, I used it in the sense as “equality”. – Zhiltsoff Igor Jul 28 '21 at 20:47
  • Okay, so a proposal of my current understanding of your question: "With this algorithm, can we prove `invmap @F id id = id` and `invmap @F f g . invmap @F f' g' = invmap @F (f . f') (g' . g)`?" Does that sound right? (Note that "`fmap` is a function which satisfies `Functor` laws" is not actually enough to pin down a single mapping -- there may be many such. So asking whether `invmap = fmap` isn't really well-formed; you have to say *which* of the many possible law-abiding `fmap`s you want to be equal to. This is what I think the closest precise thing is.) – Daniel Wagner Jul 28 '21 at 20:56
  • @DanielWagner the algorithm yields `fmap f = invariant f undefined`. I wonder whether we get the `fmap` we want when assign *contravariant processor* to be `undefined` (same for other cases.) – Zhiltsoff Igor Jul 28 '21 at 21:00
  • In order for that question to be answerable, you have to say carefully *what `fmap` we want*. – Daniel Wagner Jul 28 '21 at 21:02
  • @DanielWagner as for `fmap` we want: I’ve never really thought of the variety of `fmap`s. I don’t even know how we even choose a `fmap` when implementing manually, given that there are many variants! Do you mean difference in implementation, or different results when applied to same arguments? – Zhiltsoff Igor Jul 28 '21 at 21:04
  • Different results when applied to same arguments. – Daniel Wagner Jul 28 '21 at 21:10
  • Let us [continue this discussion in chat](https://chat.stackoverflow.com/rooms/235406/discussion-between-zhiltsoff-igor-and-daniel-wagner). – Zhiltsoff Igor Jul 29 '21 at 06:42

0 Answers0