Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Comonad duplicate function

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!

like image 650
Jackie Avatar asked Dec 03 '14 20:12

Jackie


1 Answers

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.

like image 60
Cirdec Avatar answered Nov 17 '22 21:11

Cirdec