从理论上讲，这是列表的有效comonad实例吗？

Question

我正在尝试掌握comonads的概念，在阅读了this blog post之后，我想我对它们的作用以及它们与monads的关系有了一个坚实的理解。但是，我想我应该深入研究一下这个主题，考虑一下泛型list类型的comonad实例(你知道，[a])是什么样子的，然后我发现了一个我不完全知道的东西。

因此，给出博客帖子使用的实例：

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

我认为[a]的实例声明应该是这样的( [a]的语法可能是不可能的，也可能是错误的，但您在这里得到了想法)：

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

在这里，我们只查找列表中的所有subsequences，但是只使用它的powerset或其他东西是完全可行的。在(a -> [a])形式的列表上有几个函数，对于哪一个是正确的，并不明确。

这是不是意味着不能将[a]正确地实例化为comonad，或者仅仅由用户决定cojoin将实际做什么？

Answer 1

要澄清其他人提到的内容，请考虑以下非空列表类型：

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)

您可以编写有效的comonad实例，如下所示：

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)

让我们证明hammar列出的定律。我将采取eta的自由-扩展每一个作为给定的第一步。

定律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
  _|_ = _|_

法律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
  _|_ = _|_

第三条法则。

(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
  _|_ = _|_