¿Las mónadas Writer my E son categóricamente duales?

Question

Noté que hay una relación dual entre Writer m y Either e mónadas. Si m es un monoide, entonces

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

se puede utilizar para formar una mónada:

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

El dual de() es nula (tipo vacío), el doble de producto es coproducto. Cada tipo e puede tener una estructura "comonoide":

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

de la manera obvia. Ahora,

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 

y esta es la Either e mónada. Las flechas siguen exactamente el mismo patrón.

Pregunta: ¿Es posible escribir un solo código genérico que será capaz de llevar a cabo tanto como Either e y como Writer m dependiendo del monoide dado?

Answer 1

Yo no diría que estas mónadas son categóricamente dual, sino que ambos están producidos por la construcción siguiente: dado un monoidal category (C, y otimes ;, 1) y un álgebra A en C, consideran que el envío de X mónada a A & otimes; X. En el primer caso, C es Hask, & otimes; es ×, y un álgebra es un monoide, y en el segundo caso C es Hask, & otimes; es ∐ (Either), y un álgebra es solo un tipo (cada tipo es un álgebra w.r.t. ∐ de una manera única — esto es lo que usted llama un "comonoide", aunque eso generalmente significa algo más, vea más abajo). Como es habitual, estoy trabajando en un mundo imaginario donde ⊥ no existe, por lo que × es en realidad un producto y así sucesivamente. Probablemente sea posible capturar esta generalización común usando una clase de tipo adecuada para categorías monoidales (estoy demasiado cansado para entender qué categoría-extras está tratando de hacer al respecto en este momento) y de ese modo definir simultáneamente Escritor y O bien como mónadas (modulo newtypes, posiblemente).

En cuanto a la categórica dual del escritor m — Bueno, depende de lo que desee considerar como fijo, pero el candidato más probable parece ser la estructura comonad en (,) m sin ningún tipo de condiciones en m:

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

(tenga en cuenta que aquí es donde utilizamos que m es un comonoid, es decir, tenemos mapas → m(), m m → × m).

Answer 2

en sentido estricto, () y Void no son de doble - la presencia de ⊥ significa que todos los tipos están habitadas, por lo tanto ⊥ es el único habitante de Void, lo que es un objeto terminal como era de esperar. () está habitado por dos valores, por lo que no es relevante. Si aleja manualmente then, entonces () es terminal y Void es inicial como se esperaba.

No creo que el ejemplo es una estructura comonoid, o bien - la firma de un comonoid debe ser algo como esto, pienso:

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

Lo cual, si se tiene en cuenta lo que las leyes equivalentes comonoid debe ser, termina siendo bastante inútil, creo.

Me pregunto en cambio si lo que está obteniendo está más estrechamente relacionado con los monoides de suma/producto estándar que con los naturales, tal como se aplica a los tipos de datos algebraicos. Void y Either son 0/+, mientras que () y (,) son 1/*. Pero no estoy seguro de cómo justificar el resto.

Answer 3

Aquí está el código:

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

Uso:

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