Являются ли монады Writer m и Either e категорически двойственными?

Question

Я заметил, что между монадами Writer m и Either e существует двойственное отношение. Если m является моноидом, то

unit :: () -> m
join :: (m,m) -> m

может использоваться для формирования монады:

return is composition: a -> ((),a) -> (m,a)
join is composition: (m,(m,a)) -> ((m,m),a) -> (m,a)

Двойственное из () - Void (пустой тип), двойственное из - это сопутствующий продукт. Каждому типу е можно придать «комоноидную» структуру:

unit :: Void -> e
join :: Either e e -> e

очевидным образом. Теперь,

return is composition: a -> Either Void a -> Either e a
join is composition: Either e (Either e a) -> Either (Either e e) a -> Either e a

и это монада Either e. Стрелки следуют точно так же.

Вопрос: Можно ли написать один общий код, который сможет работать как Either e и как Writer m в зависимости от заданного моноида?

Answer 1

Я бы не сказал, что эти монады категорически двойственны, скорее, они оба созданы по следующей конструкции: дана моноидальная категория (C, otimes ;, 1) и алгебра A в C рассмотрим монаду, посылающую X в A & otimes; X. В первом случае C - это Hask, & otimes; is & times; и алгебра является моноидом, а во втором случае C является Hask, & otimes; is ∐ (Либо), а алгебра - это просто тип (каждый тип является алгеброй w.r.t. unique уникальным образом - это то, что вы называете «comonoid», хотя обычно это означает что-то еще, см. ниже). Как обычно, я работаю в воображаемом мире, где ⊥ не существует, так что & times; на самом деле продукт и так далее. Вероятно, можно уловить это общее обобщение, используя подходящий класс типов для моноидальных категорий (я слишком устал, чтобы понять, что в данный момент пытаются сделать экстра-категории в этом отношении) и, таким образом, одновременно определить Writer и Either как монады ( по модулю newtypes, возможно).

Что касается категорического двойника Writer - хорошо, это зависит от того, что вы хотите считать фиксированным, но наиболее вероятным кандидатом представляется структура comonad на (,) m без каких-либо условий на m:

instance Comonad ((,) m) where
    coreturn (m, a) = a
    cojoin (m, a) = (m, (m, a))

(обратите внимание, что здесь - это то место, где мы используем, что m является комоноидом, то есть у нас есть карты m & rarr; (), m & rarr; m & times; m).

Answer 2

Вот код:

{-# LANGUAGE FlexibleInstances, EmptyDataDecls, MultiParamTypeClasses,
FunctionalDependencies, GeneralizedNewtypeDeriving, UndecidableInstances #-}

import Control.Arrow (first, second, left, right)
import Data.Monoid

data Void
data Iso a b = Iso { from :: a -> b, to :: b -> a}

-- monoidal category (Hask, m, unit)
class MonoidalCategory m unit | m -> unit where
  iso1 :: Iso (m (m x y) z) (m x (m y z))
  iso2 :: Iso x (m x unit)
  iso3 :: Iso x (m unit x)

  map1 :: (a -> b) -> (m a c -> m b c)
  map2 :: (a -> b) -> (m c a -> m c b)

instance MonoidalCategory (,) () where
  iso1 = Iso (\((x,y),z) -> (x,(y,z))) (\(x,(y,z)) -> ((x,y),z))
  iso2 = Iso (\x -> (x,())) (\(x,()) -> x)
  iso3 = Iso (\x -> ((),x)) (\((),x) -> x)
  map1 = first
  map2 = second

instance MonoidalCategory Either Void where
  iso1 = Iso f g
         where f (Left (Left x)) = Left x
               f (Left (Right x)) = Right (Left x)
               f (Right x) = Right (Right x)

               g (Left x) = Left (Left x)
               g (Right (Left x)) = Left (Right x)
               g (Right (Right x)) = Right x
  iso2 = Iso Left (\(Left x) -> x)
  iso3 = Iso Right (\(Right x) -> x)
  map1 = left
  map2 = right

-- monoid in monoidal category (Hask, c, u)
class MonoidM m c u | m -> c u where
  mult :: c m m -> m
  unit :: u -> m

-- object of monoidal category (Hask, Either, Void)
newtype Eith a = Eith { getEith :: a } deriving (Show)

-- object of monoidal category (Hask, (,), ())
newtype Monoid m => Mult m = Mult { getMult :: m } deriving (Monoid, Show)

instance MonoidM (Eith a) Either Void where
  mult (Left x) = x
  mult (Right x) = x
  unit _ = undefined

instance Monoid m => MonoidM (Mult m) (,) () where
  mult = uncurry mappend
  unit = const mempty

instance (MonoidalCategory c u, MonoidM m c u) => Monad (c m) where
  return = map1 unit . from iso3
  x >>= f = (map1 mult . to iso1) (map2 f x)

Использование:

a = (Mult "hello", 5) >>= (\x -> (Mult " world", x+1))
                                 -- (Mult {getMult = "hello world"}, 6)
inv 0 = Left (Eith "error")
inv x = Right (1/x)
b = Right 5 >>= inv              -- Right 0.2
c = Right 0 >>= inv              -- Left (Eith {getEith="error"})
d = Left (Eith "a") >>= inv      -- Left (Eith {getEith="a"})

Answer 3

Строго говоря, () и Void не являются двойственными - наличие ⊥ означает, что все типы обитаемы, поэтому ⊥ является единственным обитателем Void, что делает его конечным объектом, как вы ожидать. () содержит два значения, поэтому не имеет значения. Если вы отмахиваетесь рукой от ⊥, то () является терминальным, а Void начальным, как и ожидалось.

Я тоже не думаю, что ваш пример является comonoid структурой - подпись для comonoid должна быть примерно такой, я думаю:

class Comonoid a
    coempty :: a -> ()
    coappend :: a -> (a, a)

Что, если учесть, какими должны быть эквивалентные законы о комоноидах, в конечном итоге оказывается довольно бесполезным, я думаю.

Интересно, а вместо этого то, к чему вы обращаетесь, более тесно связано со стандартными моноидами сумма / произведение по натуральным, применяемым к алгебраическим типам данных? Void и Either равны 0 / +, тогда как () и (,) равны 1 / *. Но я не уверен, как оправдать все остальное.