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 typew a -> b
. Since these come from categories, it might be easier to reason about them in terms of a category than in terms of theComonad
laws.extract
is the identity of this category and=<=
is the composition operator.We also know that
extend f = fmap f . duplicate
, so we can writeThis 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 whenZ
represents a value at a position in a list with nothing before it.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 thatextract
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 ofextract =<= isFirst
orisFirst =<= extract
will fail for the inputZ [1] 2 []
. Both of these should be the same asisFirst $ Z [1] 2 []
, which isFalse
. We'll tryextract =<= isFirst
first, which happens to work out.When we try
isFirst =<= extract
we won't be so lucky.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 correctduplicate
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
isfmap extract . duplicate
, and this needs to be the identity function. Apparently I'm rediscovering how the laws are written in the documentation forControl.Category
. This lets us write something likeNow,
z
has only one constructor, so we can substitute that inFrom they type of duplicate, we know it must return the same constructor.
If we apply
fmap
to thisZ
we haveIf we split this up by the parts of the
Z
constructor we have three equationsThis tells us that at the very least the result of
duplicate (Z left x right)
must hold:left
for the left sideZ
withx
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
.