Why when you define the function duplicate
duplicate :: w a -> w (w a)
for the Comonad typeclass (link) you have to modify all the elements "in the context" (i.e. change elements other than the current value of the context). Why not just use something like return in a Monad?
Example (zipper):
data Z a = Z [a] a [a]
why cannot I just define duplicate as
duplicate z = Z [] z []
I tried to derive a requirement for the duplicate function from the Comonad rules, but I always end up with a duplicate which just wraps the element much like a return in a monad without any need to do anything else.
One blog post says:
duplicate is a bit harder to grasp. From a list zipper, we have to build a list zipper of list zippers. The signification behind this (confirmed by the comonad laws that every instance has to fulfill) is that moving inside the duplicated structure returns the original structure, altered by the same move
But I don't understand why it must be that way. The fmap in the Comonad rules always applies to the wrapped element and afterwards this one element is always "unwrapped" with extract, why bother doing anything else in the duplicate function other than just wrapping the argument of duplicate?
Can you point out what I have missed? I feel like I made some obvious error somewhere, but I just cannot figure it out on my own.
Thanks in advance for you replies!
It's important if you can do other things with the type than simply extract
from it. Intuitively, if the only thing you can do is extract the value, then the type only holds one value, so duplicating that one value is duplicating everything. This isn't true in general, and it's not true for zippers.
The Comonad
laws are just the category laws in disguise on functions of the type w a -> b
. Since these come from categories, it might be easier to reason about them in terms of a category than in terms of the Comonad
laws. extract
is the identity of this category and =<=
is the composition operator.
-- | Right-to-left 'Cokleisli' composition
(=<=) :: Comonad w => (w b -> c) -> (w a -> b) -> w a -> c
f =<= g = f . extend g
We also know that extend f = fmap f . duplicate
, so we can write
f =<= g = f . fmap g . duplicate
This looks fairly easy to reason about. Now, let's equip your Z
type with another function that we can talk about. isFirst
will return true only when Z
represents a value at a position in a list with nothing before it.
isFirst :: Z a -> Bool
isFirst (Z [] _ _) = True
isFirst _ = False
Now, let's consider what happens when we use isFirst
with the three category laws. The only two it seems are immediately applicable to it are that extract
is a left and right identity for composition by =<=
. Since we are only disproving this, we only need to find a counter-example. I suspect that one of extract =<= isFirst
or isFirst =<= extract
will fail for the input Z [1] 2 []
. Both of these should be the same as isFirst $ Z [1] 2 []
, which is False
. We'll try extract =<= isFirst
first, which happens to work out.
extract =<= isFirst $ Z [1] 2 []
extract . fmap isFirst . duplicate $ Z [1] 2 []
extract . fmap isFirst $ Z [] (Z [1] 2 []) []
extract $ Z [] (isFirst (Z [1] 2 [])) []
extract $ Z [] False []
False
When we try isFirst =<= extract
we won't be so lucky.
isFirst =<= extract $ Z [1] 2 []
isFirst . fmap extract . duplicate $ Z [1] 2 []
isFirst . fmap extract $ Z [] (Z [1] 2 []) []
isFirst $ Z [] (extract (Z [1] 2 [])) []
isFirst $ Z [] 2 []
True
When we duplicate
d we lost information about the structure. In fact, we lost information about everything that came everywhere except the single focal point of the zipper. The correct duplicate
would have has a whole 'nother zipper everywhere in the context holding the value at that location and that location's context.
Let's see what we can deduce from these laws. With a little hand waving about the category of functions, we can see that =<= extract
is fmap extract . duplicate
, and this needs to be the identity function. Apparently I'm rediscovering how the laws are written in the documentation for Control.Category
. This lets us write something like
z = (=<= extract) z
z = fmap extract . duplicate $ z
Now, z
has only one constructor, so we can substitute that in
Z left x right = fmap extract . duplicate $ Z left x right
From they type of duplicate, we know it must return the same constructor.
Z left x right = fmap extract $ Z lefts (Z l x' r) rights
If we apply fmap
to this Z
we have
Z left x right = Z (fmap extract lefts) (extract (Z l x' r)) (fmap extract rights)
If we split this up by the parts of the Z
constructor we have three equations
left = fmap extract lefts
x = extract (Z l x' r)
right = fmap extract rights
This tells us that at the very least the result of duplicate (Z left x right)
must hold:
left
for the left sideZ
with x
in the middle for the middleright
for the right sideFurthermore, we can see that the middle values in the lists on the left and right side must be the same as the original values in those lists. Considering just this one law we know enough to demand a different structure for the result of duplicate
.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With