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

Question

我正在努力掌握comonads的概念,在阅读了这篇博文之后,我想我对他们的工作以及他们与monad的关系有了深刻的理解.但是,我想我会深入研究这个主题,只考虑一下通用列表类型的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

如评论中所述,对于可能为空的列表,您不能拥有comonad实例,因为coreturn必须返回一些内容.

除此之外,您的实例还必须满足comonad法律.表达为coreturn和cojoin,这些是:

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

即使我们禁止空列表,您也可以轻松地看到这些内容不适用于您的实例.但是,假设coreturn是这样head,我们可以使用这些法则来获得cojoin必要的线索.

从(1),我们可以确定返回的列表的第一个元素cojoin必须是原始列表,并且从(2)我们看到组合每个内部列表的第一个元素也必须产生原始列表.这强烈暗示我们需要类似tails^*的东西,并且可以确认这也满足(3).

_{^*更具体地说,我们需要一个版本tails,最后不包括空列表.}

Answer 2

为了澄清其他人提到的内容,请考虑非空列表的以下类型:

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)

让我们来证明哈马尔列出的法律.作为给定的第一步,我将自由地扩展每一个.

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

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