Разумные реализации Comonad

Question

Мы можем описать монаду как вычислительный контекст, и реализация монады точно сохраняет значение этого контекста. Например, Option - контекст означает, что значение может существовать. Учитывая тип данных Option, единственная реализация, которая имеет смысл, pure = some, flatMap f = {none => none; some x => f x }Как я понимаю, монады, следуя сигнатурам типов - есть только одна разумная реализация для любой монады. Другими словами, если вы хотите добавить значимый контекст к значению / вычислению, существует только один способ сделать это для любой конкретной монады.
С другой стороны, когда дело доходит до comonad, он внезапно начинает чувствовать себя совершенно странно, как будто есть много способов реализовать comonad для данного типа, и вы могли бы даже дать определенный смысл для каждой реализации.
Рассмотрим, NEL, с copure = head, cojoin реализуется через tails, который прекрасно удовлетворяет типам. Если мы реализуем cojoin от permutations или как fa map (_ => fa) map f это не будет удовлетворять законам комонад.
Но круговая реализация действительна:

override def cobind[A, B](fa: NonEmptyList[A])(f: (NonEmptyList[A]) => B): NonEmptyList[B] = {
  val n: NonEmptyList[NonEmptyList[A]] = fa.map(_ => fa).zipWithIndex.map { case (li , i ) =>
    val(h: List[A], t: List[A]) = li.list.splitAt(i)
    val ll: List[A] = t ++ h
    NonEmptyList.nel(ll.head, ll.tail)
  }
  n map f
}

Причина такой двусмысленности для Командования, даже несмотря на то, что законы, ограничивающие нас, на мой взгляд, в том, что если в Монаде мы ограничиваем себя в каком-то контексте (мы не можем "создавать" новую информацию), то в Комонаде мы дальнейшее расширение этого контекста (есть целый ряд способов составить список списков из списка), что дает нам больше возможностей сделать это. В моей голове метафора: для Монады мы стоим на дороге и хотим достичь некоторых точка назначения A =, следовательно, существует только кратчайший путь выбора. В команде мы стоим в точке A и хотим куда-то от нее уйти, так что есть и другие способы сделать это.
Итак, мой вопрос - я действительно прав? Можем ли мы реализовать команду по-разному, каждый раз делая еще одну значимую абстракцию? Или только реализация хвостов является разумной, поскольку абстракция, которую предполагает вводить comonad.

Answer 1

Непустые списки возникают как две отдельные комонады двумя стандартными конструкциями.

Во-первых, cofree comonad дается таким образом.

data Cofree f x = x :& f (Cofree f x)  -- every node is labelled with an x

instance Functor f => Functor (Cofree f) where
  fmap f (x :& fcx) = f x :& fmap (fmap f) fcx

instance Functor f => Comonad (Cofree f) where
  extract (x :& _) = x   -- get the label of the top node
  duplicate cx@(_ :& fcx) = cx :& fmap duplicate fcx

Непустые списки могут быть даны как

type Nellist1 = Cofree Maybe

и, таким образом, автоматически запутанные. Это дает вам "хвосты" комонады.

Между тем, разложение структуры как "молнии элемента" индуцирует комонадную структуру. Как я объяснил очень подробно,

Дифференцируемость сводится к этой группе операций с застежками-молниями (отдельные элементы выбираются из контекста и помещаются "в фокус")

class (Functor f, Functor (DF f)) => Diff1 f where
  type DF f :: * -> *
  upF      ::  ZF f x  ->  f x           -- defocus
  downF    ::  f x     ->  f (ZF f x)    -- find all ways to focus
  aroundF  ::  ZF f x  ->  ZF f (ZF f x) -- find all ways to *re*focus

data ZF f x = (:<-:) {cxF :: DF f x, elF :: x}

таким образом, мы получаем функтор и комонаду

instance Diff1 f => Functor (ZF f) where
  fmap f (df :<-: x) = fmap f df :<-: f x

instance Diff1 f => Comonad (ZF f) where
  extract    = elF
  duplicate  = aroundF

В принципе, при этой конструкции возникают и непустые списки. Проблема в том, что дифференцируемый функтор не так легко выразить в Хаскеле, хотя его производная разумна. Давай сойдем с ума...

Непустые списки составляют ZF thingy x где DF thingy = [], Можем ли мы интегрировать списки? Дурачиться алгебраически может дать нам ключ

[x] = Either () (x, [x]) = 1 + x * [x]

так что в степенной серии мы получаем

[x] = Sum(n :: Nat). x^n

и мы можем интегрировать степенные ряды

Integral [x] dx = Sum(n :: Nat). x^(n+1)/(n+1)

Это означает, что мы получаем произвольные наборы размера (n+1), но мы должны идентифицировать их с точностью до некоторого отношения, где классы эквивалентности имеют размер (n+1). Один из способов сделать это - определить кортежи до поворота, чтобы вы не знали, какая из (n + 1) позиций является "первой".

То есть списки являются производными непустых циклов. Подумайте о людях за круглым столом, играющих в карты (возможно, пасьянс). Поверните стол, и вы получите ту же самую группу людей, играющих в карты. Но как только вы назначаете дилера, вы фиксируете список других игроков по порядку, начиная по часовой стрелке слева от дилера.

Две стандартные конструкции; две комонады для одного и того же функтора.

(В своем комментарии ранее я отмечал возможность использования нескольких монад. Это немного связано, но вот отправная точка. Каждая монада m также является аппликативным, и m () моноид Соответственно, каждая моноидная структура для m () по крайней мере, дает кандидата на структуру монады на m, В случае писателя монады (,) sполучаем, что кандидатами в монады являются моноиды на (s,()) которые так же, как моноиды на s.)

Редактирование непустых списков также монадическое, по крайней мере, двумя различными способами.

Я определяю тождество и спаривание для функторов следующим образом.

newtype I         x = I x
data    (f :*: g) x = (:&:) {lll :: f x, rrr :: g x}

Теперь я могу ввести непустые списки следующим образом, а затем определить конкатенацию.

newtype Ne x = Ne ((I :*: []) x)

cat :: Ne x -> Ne x -> Ne x
cat (Ne (I x :&: xs)) (Ne (I y :&: ys)) = Ne (I x :&: (xs ++ y : ys))

Они монадические, как и пустые списки:

instance Monad Ne where
  return x = Ne (I x :&: [])
  Ne (I x :&: xs) >>= k = foldl cat (k x) (map k xs)

Тем не мение, I это монада:

instance Monad I where
  return = I
  I a >>= k = k a

Более того, монады закрыты при спаривании:

instance (Monad f, Monad g) => Monad (f :*: g) where
  return x = return x :&: return x
  (fa :&: ga) >>= k = (fa >>= (lll . k)) :&: (ga >>= (rrr . k))

Таким образом, мы могли бы просто написать

newtype Ne x = Ne ((I :*: []) x) deriving (Monad, Applicative, Functor)

но return ибо эта монада дает нам двойное видение.

return x = Ne (I x :&: [x])

Итак, вы здесь: непустые списки - это двоякие, двунаправленные, однонаправленные шесть способов,...

(Много можно сказать по этому поводу, но я должен где-то остановиться.)

Answer 2

Вот тот же контрпример, показывающий, что у Monad есть несколько возможных экземпляров, от комментария свиновода, но более проработанный (хотя и не проверенный на наличие ошибок, поэтому извините за любые ошибки).

data WithBool a = WB Bool a deriving Functor

instance Monad WithBool where
     return = WB z
     (WithBool b a) >>= f =
           case f a of (WithBool b2 r) -> WithBool (b `op` b2) r

-- This holds if op = (&&) and z = True
-- This also holds if op = (||) and z = False
-- It should also work if op = const or `flip const` and z = True _or_ False

Как говорит Бакуриу, выбор реализации "по умолчанию", таким образом, несколько произвольный и обусловлен тем, что от людей ожидают.