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

Question

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

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

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

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

Двойной из() является ничтожным (пустым типом), двойственное продукта копроизведение. Каждому типу e может быть присвоена структура «comonoid»:

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

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

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

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

(обратите внимание, что здесь где мы используем, что т является comonoid, т.е. мы имеем карту м →(), м → м × м).

Answer 2

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

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

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

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

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

Answer 3

Вот код:

{-# 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"})