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

Мы можем описать монаду как вычислительный контекст, и реализация монады в точности сохраняет значение этого контекста. Например, Option — контекст означает, что значение может существовать. Учитывая тип данных Option, единственная реализация, которая имеет смысл, это pure = some, flatMap f = {none => none; some x => f x } Как я понимаю монады, следуя сигнатурам типов - есть только одна разумная реализация для любой монады. Другими словами, если вы хотите добавить какой-то осмысленный контекст к значению/вычислению, есть только один способ сделать это для любой конкретной монады.
С другой стороны, когда дело доходит до комонады, это внезапно начинает казаться совершенно странным, как будто есть много-много способов реализовать комонаду для данного типа, и вы можете даже дать определенное значение для каждой реализации.
Рассмотрим, 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 и хотим куда-то отправиться из нее, так что есть гораздо больше способов сделать это.
Итак, мой вопрос: Я на самом деле прав? Можем ли мы реализовать команду по-разному, каждый раз делая новую осмысленную абстракцию? Или только реализация хвостов является разумной из-за абстракции, которую должна привнести комонада.


functional-programming haskell scalaz comonad
person I See Voices    schedule 04.03.2016    source источник
comment
Неверно предполагать, что данный оператор типа имеет не более одной монадной реализации. Например, соединение с логическим значением имеет как минимум столько же реализаций монад, сколько моноидов в логических значениях, поэтому и, или, исключающее или, равенство дают разные монады. Тармо Уусталу дает очень красивую комбинаторную трактовку этого вопроса, перечисляя возможные (ко)монадные структуры для данного оператора контейнерного типа. Ключ действительно состоит в том, чтобы идентифицировать моноидные структуры на основных формах и позициях контейнера. Они, как правило, далеко не уникальны.   -  person pigworker    schedule 04.03.2016
comment
Спасибо! Означает ли это, что любая реализация Monad/Comonad, удовлетворяющая законам, имеет смысл? И почему тогда, например, реализация кобинда Nel по умолчанию осуществляется через хвосты?   -  person I See Voices    schedule 04.03.2016
comment
@ISeeVoices имеет смысл, не имеет значения. Любая монада/комонада, удовлетворяющая законам, обладает определенными заданными свойствами, и точка. Можно ли использовать эти свойства и использовать их для получения чего-то полезного — это другой вопрос, который зависит от того, с чем вы имеете дело и чего хотите достичь, но нет способа формально определить полезную монаду или полезную комонаду. Реализация по умолчанию была выбрана разработчиками языка на основе их мнения о том, какая из них более полезна; мнение, которое, надеюсь, основано на реальном жизненном опыте использования экземпляров.   -  person Bakuriu    schedule 04.03.2016
comment
@pigworker, у вас есть цитата из газеты Uustalu?   -  person sclv    schedule 04.03.2016
comment
@sclv Начните здесь и следуйте своему носу.   -  person pigworker    schedule 04.03.2016

Ответы (2)


arrow_upward
8
arrow_downward

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

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

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

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

Непустые списки составляют 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])

Итак, вы здесь: непустые списки являются комонадными двумя способами, монадическими двумя способами, аппликативными шестью способами,...

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

person pigworker    schedule 04.03.2016

arrow_upward
1
arrow_downward

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

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

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

person sclv    schedule 04.03.2016
comment
спасибо всем, теперь немного понятнее. Итак, законы гарантируют нам определенное поведение, но смысл их выполнения мы должны найти сами. - person I See Voices; 04.03.2016