This Reddit post by Edward Kmett provides a constructive definition of a natural map, the one from the free theorem for fmap
(which I read in yet another Edward Kmett's post):
For given
f
,g
,h
andk
, such thatf . g = h . k
:$map f . fmap g = fmap h . $map k
, where$map
is the natural map for the given constructor.
I do not fully understand the algorithm. Let us approach it step-by-step:
We can define a "natural map" by induction over any particular concrete choice of
F
you give. Ultimately any such ADT is made out of sums, products,(->)
's,1
s,0
s,a
's, invocations of other functors, etc.
Consider:
data Smth a = A a a a | B a (Maybe a) | U | Z Void deriving ...
No arrows. Let us see how fmap
(which I reckon to be the natural choice for any ADT without (->)
s in it) would operate here:
instance Functor Smth where
fmap xy (A x x1 x2) = A (xy x) (xy x1) (xy x2)
fmap xy (B x xPlus1) = B (xy x) (fmap xy xPlus1)
-- One can pattern-match 'xPlus1' as 'Just x1' and 'Nothing'.
-- From my point of view, 'fmap' suits better here. Reasons below.
fmap _xy U = U
fmap _xy (Z z) = absurd z
Which seems natural. To put this more formally, we apply xy
to every x
, apply fmap xy
to every T x
, where T
is a Functor
, we leave every unit unchanged, and we pass every Void
onto absurd
. This works for recursive definitions too!
data Lst a = Unit | Prepend a (Lst a) deriving ...
instance Functor Lst where
fmap xy Unit = Unit
fmap xy (Prepend x lstX) = Prepend (xy x) (fmap xy lstX)
And for the non-inductive types:(Detailed explanation in this answer under the linked post.)
Graph a = Node a [Graph a]
instance Functor Graph where
fmap xy (Node x children) = Node (xy x) (fmap (fmap xy) children)
This part is clear.
When we allow
(->)
we now have the first thing that mixes variance up. The left-hand type argument of(->)
is in contravariant position, the right-hand side is in covariant position. So you need to track the final type variable through the entire ADT and see if it occurs in positive and/or negative position.
Now we include (->)
s. Let us try to keep this induction going:
We somehow derived natural maps for T a
and S a
. Thus, we want to consider the following:
data T2S a = T2S (T a -> S a)
instance ?Class? T2S where
?map? ?? (T2S tx2sx) = T2S $ \ ty -> ???
And I believe this to be the point where we start choosing. We have the following options:
- (Phantom)
a
occurs neither inT
nor inS
.a
inT2S
is phantom, thus, we can implement bothfmap
andcontramap
asconst phantom
. - (Covariant)
a
occurs inS a
and does not occur inT a
. Thus, this something among the lines ofReaderT
withS a
(which does not actually depend ona
) as environment, which substitutes?Class?
withFunctor
,?map?
withfmap
,???
,??
withxy
with:let tx = phantom ty sx = tx2sx tx sy = fmap xy sx in sy
- (Contravariant)
a
occurs inT a
and does not occur inS a
. I do not see a way to make this thing a covariant functor, so we implement aContravariant
instance here, which substitutes?map?
withcontramap
,??
withyx
,???
with:let tx = fmap yx ty sx = tx2sx tx sy = phantom sx in sy
- (Invariant)
a
occurs both inT a
andS a
. We can no longer usephantom
, which came in quite handy. There is a moduleData.Functor.Invariant
by Edward Kmett. It provides the following class with a map:
And yet, I cannot see a way to turn this into something we can pluf into the free theorem for fmap - the type requires an additional function-argument, which we can't brush off asclass Invariant f where invmap :: (a -> b) -> (b -> a) -> f a -> f b -- and some generic stuff...
id
or something. Anyway, we putinvmap
instead of?map?
,xy yx
instead of??
, and the following instead of???
:let tx = fmap yx ty sx = tx2sx tx sy = fmap xy sx in sy
So, is my understanding of such an algorithm correct? If so, how are we to properly process the Invariant case?
I think your algorithm is too complex, because you are trying to write one algorithm. Writing two algorithms instead makes things much simpler. One algorithm will build the natural fmap, and the other will build the natural contramap. BUT both algorithms need to be nondeterministic in the following sense: there will be types where they cannot succeed, and so do not return an implementation; and there will be types where there are multiple ways they can succeed, but they're all equivalent.
To start, let's carefully define what it means to be a parameterized type. Here's the different kinds of parameterized types we can have:
In
Const X
, theX
ranges over all concrete, non-parameterized types, likeInt
andBool
and so forth. And here's their interpretation, i.e. the concrete type they are isomorphic to once given a parameter:Now we can give our two algorithms. The first bit you've already written yourself:
These correspond to the clauses you gave in your first instance. Then, in your
[Graph a]
example, you gave a clause corresponding to this:That's fine, but this is also the first moment where we get some nondeterminism. One way to make this a functor is indeed nested
fmap
s; but another way is nestedcontramap
s.If both clauses are possible, then there are no
Id
s in eitherF
orF'
, so both instances will returnx
unchanged.The only thing left now is the arrow case, the one you ask about. But it turns out it's very easy in this formalism, there is only one choice:
That's the whole algorithm, in full detail, for defining the natural
fmap
. ...except one detail, which is the algorithm for the naturalcontramap
. But hopefully if you followed all of the above, you can reproduce that algorithm yourself. I encourage you to give it a shot, then check your answers against mine below.One thing of interest to me personally: it turns out that
contramap @(Id)
is the only leaf case that fails. All further failures are inductive failures ultimately deriving from this one -- a fact I had never thought of before! (The dual statement is that it turns out thatfmap @(Id)
is the only leaf case that actually uses its first function argument.)