Теоретически, это действительный экземпляр comonad для списка?

Я пытаюсь понять концепцию comonads, и после прочтения этого сообщения в блоге, я думаю, что у меня есть четкое понимание того, что они делают и как они связанные с монадами. Но я подумал, что немного углубился бы в тему и подумал бы о том, как будет выглядеть экземпляр 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?

Ответ 1

Как отмечено в комментариях, вы не можете иметь экземпляр comonad для списков, которые могут быть пустыми, поскольку coreturn должен что-то возвращать.

Кроме того, ваш пример также должен удовлетворять законам comonad. Выраженные в терминах coreturn и cojoin, это:

coreturn . cojoin = id
fmap coreturn . cojoin = id
cojoin . cojoin = fmap cojoin . cojoin

Вы можете легко убедиться, что это не относится к вашему экземпляру, даже если мы запретили пустые списки. Однако, предполагая, что coreturn head, мы можем использовать эти законы, чтобы получить некоторые подсказки относительно того, что должно быть cojoin.

Из (1) мы можем определить, что первый элемент списка, возвращаемый cojoin, должен быть исходным списком, а из (2) мы видим, что объединение первых элементов каждого внутреннего списка также должно давать исходный один. Это говорит о том, что нам нужно что-то вроде tails ^* и можно подтвердить, что это также удовлетворяет (3).

_{^* В частности, нам нужна версия tails, которая не включает пустой список в конце.}

Ответ 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 [email protected](One _) = One l
tails [email protected](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
  _|_ = _|_