15

我正在尝试掌握 monads 的概念，在阅读了这篇博文之后，我想我对它们的作用以及它们与 monads 的关系有了一个深刻的理解。但是，我想我会深入研究一下这个主题，然后想想通用列表类型（你知道，[a]）的comonad 实例会是什么样子，我发现了一个我不完全知道的是正确的。

因此，鉴于博客文章使用的实例：

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

我认为 for 的实例声明[a]看起来像这样（for 的语法[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实际做什么？

4

2 回答 2

21

如评论中所述，您不能为可能为空的列表创建一个comonad 实例，因为coreturn必须返回something。

除此之外，您的实例还必须满足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不包含末尾空列表的版本。

于 2012-09-21T20:21:46.750 回答
13

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

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)

让我们证明哈马尔列出的定律。作为给定的第一步，我将冒昧地对每一个进行 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
  _|_ = _|_

法 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
  _|_ = _|_
于 2012-09-21T21:56:21.497 回答