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?
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:
coreturn . cojoin = id
fmap coreturn . cojoin = id
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.
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
_|_ = _|_
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