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 duplicated 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:
- a list with the same length as
left for the left side
- a
Z with x in the middle for the middle
- a list with the same length as
right for the right side
Furthermore, 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.
