Theoretically, is this a valid comonad instance for a list?

Question

I'm trying to grasp the concept of comonads, and after reading this blog post, I think I have a solid understand of what they do and how they are related to monads. But, I thought I would delve into the subject a little bit and just think about what the comonad instance of the generic list type (you know, [a]) would look like, and I've come to a piece I don't fully know is correct.

So, given the instance that the blog post used:

class Functor w => Comonad w where
    (=>>)    :: w a -> (w a -> b) -> w b
    coreturn :: w a -> a
    cojoin     :: w a -> w (w a)

I thought that the instance declaration for [a] would look something like this (the syntax for [a] is probably either impossible or wrong, but you get the idea here):

instance Comonad [a] where
    coreturn = head
    cojoin = Data.List.subsequences --this is what I'm confused about
    x =>> f = map f (cojoin x)

Here, we just find all of the subsequences of the list, but it would be entirely feasible to just use it's powerset or something. There are several functions on lists of the form (a -> [a]), and it's sort of ambiguous as to which one is correct.

Does this mean that [a] cannot be properly instantiated properly as a comonad, or is it simply up to the user to decide what cojoin will actually do?

Answer 1

As noted in the comments, you cannot have a comonad instance for lists that may be empty since coreturn has to return something.

Apart from that, your instance also has to satisfy the comonad laws. Expressed in terms of coreturn and cojoin, these are:

1. coreturn . cojoin = id
2. fmap coreturn . cojoin = id
3. cojoin . cojoin = fmap cojoin . cojoin

You can easily see that these do not hold for your instance even if we disallow empty lists. However, assuming that coreturn is head, we can use these laws to get some clues as to what cojoin must be.

From (1), we can determine that the first element of the list returned by cojoin must be the original list, and from (2) we see that combining the first elements of each inner list must also yield the original one. This strongly suggests that we need something like tails^*, and it can be confirmed that this satisfies (3) as well.

_{^* More specifically, we need a version of tails that does not include the empty list at the end.}

Answer 2

To clarify upon what others have mentioned, consider the following type for non-empty lists:

data NonEmptyList a = One a | Many a (NonEmptyList a)

map :: (a -> b) -> NonEmptyList a -> NonEmptyList b
map f (One x) = One (f x)
map f (Many x xs) = Many (f x) (map f xs)

(++) :: NonEmptyList a -> NonEmptyList a -> NonEmptyList a
One x     ++ ys = Many x ys
Many x xs ++ ys = Many x (xs ++ ys)

tails :: NonEmptyList a -> NonEmptyList (NonEmptyList a)
tails l@(One _) = One l
tails l@(Many _ xs) = Many l (tails xs)

You can write a valid comonad instance as follows:

instance Functor NonEmptyList where
  fmap = map

instance Comonad NonEmptyList where
  coreturn (One x) = x
  coreturn (Many x xs) = x

  cojoin = tails

  -- this should be a default implementation
  x =>> f = fmap f (cojoin x)

Let's prove the laws listed by hammar. I'll take the liberty of eta-expanding each one as a given first step.

Law 1.

(coreturn . cojoin) xs = id xs
-- definition of `.`, `cojoin`, and `id`
(coreturn (tails xs) = xs
-- case on xs
  -- assume xs is (One x)
  (coreturn (tails (One x))) = One x
  -- definition of tails
  (coreturn (One (One x))) = One x
  -- definition of coreturn
  One x = One x

  -- assume xs is (Many y ys)
  (coreturn (tails (Many y ys))) = Many y ys
  -- definition of tails
  (coreturn (Many (Many y ys) (tails ys)) = Many y ys
  -- definition of coreturn
  Many y ys = Many y ys

  -- assume xs is _|_
  (coreturn (tails _|_)) = _|_
  -- tails pattern matches on its argument
  (coreturn _|_) = _|_
  -- coreturn pattern matches on its argument
  _|_ = _|_

Law 2.

(fmap coreturn . cojoin) xs = id xs
-- definition of `.`, `cojoin`, `fmap`, and `id`
map coreturn (tails xs) = xs
-- case on xs
  -- assume xs is (One x)
  map coreturn (tails (One x)) = One x
  -- defn of tails
  map coreturn (One (One x)) = One x
  -- defn of map
  One (coreturn (One x)) = One x
  -- defn of coreturn 
  One x = One x

  -- assume xs is (Many y ys)
  map coreturn (tails (Many y ys)) = Many y ys
  -- defn of tails
  map coreturn (Many (Many y ys) (tails ys)) = Many y ys
  -- defn of map
  Many (coreturn (Many y ys)) (map coreturn (tails ys)) = Many y ys
  -- defn of coreturn
  Many y (map coreturn (tail ys)) = Many y ys
  -- eliminate matching portions
  map coreturn (tail ys) = ys
  -- wave hands.
  -- If the list is not self-referential,
  -- then this can be alleviated by an inductive hypothesis.
  -- If not, then you can probably prove it anyways.

  -- assume xs = _|_
  map coreturn (tails _|_) = _|_
  -- tails matches on its argument
  map coreturn _|_ = _|_
  -- map matches on its second argument
  _|_ = _|_

Law 3.

(cojoin . cojoin) xs = (fmap cojoin . cojoin) xs
-- defn of `.`, `fmap`, and `cojoin`
tails (tails xs) = map tails (tails xs)
-- case on xs
  -- assume xs = One x
  tails (tails (One x)) = map tails (tails (One x))
  -- defn of tails, both sides
  tails (One (One x)) = map tails (One (One x))
  -- defn of map
  tails (One (One x)) = One (tails (One x))
  -- defn of tails, both sides
  One (One (One x)) = One (One (One x))

  -- assume xs = Many y ys
  (this gets ugly. left as exercise to reader)

  -- assume xs = _|_
  tails (tails _|_) = map tails (tails _|_)
  -- tails matches on its argument
  tails _|_ = map tails _|_
  -- tails matches on its argument, map matches on its second argument
  _|_ = _|_