Lector, escritor mónadas

Deje que $C$ sea ​​un CCC . Vamos a $(\times)$ sea un producto en bifuntor $C$ . Como Cat es CCC, podemos curry $(\times)$ :

$curry (\times) : C \rightarrow(C \Rightarrow C)$

$curry (\times) A = \lambda B. A \times B$

La categoría de functor $C \Rightarrow C$ tiene una estructura monoidal habitual. A monoid en $C \Rightarrow C$ es una mónada en $C$ . Consideramos productos finitos como la estructura de monoidal $C$ .

$curry (\times) 1 \cong id$

$\forall A\ B. curry (\times) (A\times B) \cong (curry (\times) A) \circ (curry (\times) B)$

Por lo tanto $(curry (\times))$ conserva la estructura monoidal, por lo que transporta un monoide a una mónada y un comonoide a una comonad. A saber, transporta un monoide arbitrario a mónada (mira la definición - debe ser un monoide). Del mismo modo, transporta el comonoide diagonal al comandante Coreader.( W r i t e r w )$w$$(Writer\ w)$$w$

Ahora, para concretar, despliego la construcción de Writer.

Empezar. En realidad, $Writer = Coreader = curry(\times)$ , simplemente tienen nombres distintos en Haskell. Tenemos un monoid Haskell $\langle w, mappend, mempty\rangle$ :

$mappend : w\times w \to w$

$mempty : 1 \to w$

Writer es un functor, por lo que debe mapear también los morfismos, como $mappend$ y $mempty$ . Escribo esto como a continuación, aunque no es válido en Haskell:

$Writer\ mappend : Writer(w\times w) \to Writer\ w$

es una transformación natural, un morfismo en C ⇒ C . Por propiedades de c u r r y ( × ) es una función, que toma a ∈ O b ( C ) y da un morfismo en C :$Writer\ mappend$$C\Rightarrow C$$curry(\times)$$a \in Ob(C)$$C$

$Writer\ mappend\ a = mappend\times(id(a)) : Writer (w\times w) a \to Writer\ w\ a$

De manera informal, sumas componentes de tipo w y bombas un intacta. Esta es exactamente la definición de escritor en Haskell. Uno de los obstáculos es que para la mónada ⟨ W r i t e r w , μ , eta ⟩ necesitamos$Writer\ mappend\ a$$w$$a$$\langle Writer\ w,\mu,\eta\rangle$

$\mu : Writer\ w \circ Writer\ w \to Writer\ w$

es decir, incompatibilidad de tipos. Pero estos functores son isomórficos: por el asociador habitual para productos finitos que es un isomorfismo natural ≅ λ a . w × ( w × a ) = W r i t e r w ∘ W r i t e r $Writer (w\times w) = \lambda a. (w\times w)\times a$$\cong \lambda a. w\times(w\times a) = Writer\ w \circ Writer\ w$. Luego definimos vía W r i t e r m a p p e n d . Omito una construcción de η a través de m e m p t y .$\mu$$Writer\ mappend$$\eta$$mempty$

Escritor, siendo un funtor, conserva diagrama conmutativo, es decir, conservas monoid igualdades, por lo que tenemos para igualdades probadas concedidas para = a monoid en ( C ⇒ C ) = a mónada en C . Final.$\langle Writer\ w,\mu,\eta\rangle$$(C\Rightarrow C)$$C$

¿Qué pasa con Reader y Cowriter? Reader es adjunto a Coreader, como se explica en la definición de Coreader, ver enlace arriba. Del mismo modo, Cowriter es adjunto al escritor. No encontré una definición de Cowriter, así que la inventé por analogía en la tabla:

{- base, Hackage.category-extras -}
import Control.Comonad
import Data.Monoid
data Cowriter w a = Cowriter (w -> a)
instance Functor (Cowriter w) where
    fmap f (Cowriter g) = Cowriter (f . g)
instance Monoid w => Copointed (Cowriter w) where
    extract (Cowriter g) = g mempty
instance Monoid w => Comonad (Cowriter w) where
    duplicate (Cowriter g) = Cowriter
        (\w' -> Cowriter (\w -> g (w `mappend` w')))

A continuación se encuentran las definiciones simplificadas de esas (co) mónadas. fr_ob F denota un mapeo de un functor F en objetos, fr_mor F denota un mapeo de un functor F en morfismos. Hay un objeto monoid en C .$\langle w,\hat{+},\hat{0}\rangle$$C$

• Escritor
  • $fr\_ob (Writer\ w) a = a\times w$
  • $fr\_mor (Writer\ w) f = \lambda \langle a_0,w_2\rangle. \langle a_0,f\ w_2\rangle$
  • $\eta a = \lambda a_0. \langle a_0, \hat{0} \rangle$
  • $\mu a = \lambda \langle \langle a_0,w_1\rangle,w_0\rangle. \langle a_0, w_0\hat{+}w_1\rangle$
• Lector
  • $fr\_ob (Reader\ r) a = r\to a$
  • $fr\_mor (Reader\ r) f = \lambda g\ r_0. f (g\ r_0)$
  • $\eta a = \lambda a_0\ r_0. a_0$
  • $\mu a = \lambda f\ r_0. f\ r_0\ r_0$
• Coreader
  • $fr\_ob (Coreader\ r) a = r\times a$
  • $fr\_mor (Coreader\ r) f = \lambda \langle r_0,a_0\rangle. \langle f\ r_0,a_0\rangle$
  • $\eta a = \lambda \langle r_0,a_0\rangle. a_0$
  • $\mu a = \lambda \langle r_0,a_0\rangle. \langle r_0,\langle r_0,a_0\rangle\rangle$
• Cowriter
  • $fr\_ob (Cowriter\ w) a = w\to a$
  • $fr\_mor (Cowriter\ w) f = \lambda g\ r_0. f (g\ r_0)$
  • $\eta a = \lambda f. f\ \hat{0}$
  • $\mu a = \lambda f\ w_1 w_0. f (w_0\hat{+}w_1)$

La pregunta es que el adjunto en relaciona a los functores, no a las mónadas. No veo cómo el adjunto implica "Coreader es una comonad" → "Reader es una mónada" y "Writer es una mónada" → "Cowriter es una comonad".$C$$\to$$\to$

Observación. Estoy luchando por proporcionar más contexto. Requiere algo de trabajo. Especialmente, si necesita pureza categórica y esas (co) mónadas fueron introducidas para programadores. Sigue regañando! ;)

Yes, if a monad $M : C \to C$ has a right adjoint $N$, then $N$ automatically inherits a comonad structure.

The general category-theoretic setting to understand this is as follows. Let $C$ and $D$ be two categories. Write $\mathrm{Fun}(C, D)$ for the categeory of functors from $C$ to $D$; Its objects are functors and its morphisms natural transformations. Write $\mathrm{Fun}^L(C, D)$ for the full subcategory of $\mathrm{Fun}(C, D)$ on the functors which have right adjoints (in other words, we consider functors $C \to D$ with right adjoints and arbitrary natural transformations between them). Write $F^R : D \to C$ for the right adjoint of a functor $F : C \to D$. Then $-^R : \mathrm{Fun}^L(C, D) \to \mathrm{Fun}(D, C)$ is a contravariant functor: if $\alpha : F \to G$ is a natural transformation then there is an induced natural transformation $\alpha^R : G^R \to F^R$.

$C = D$$\mathrm{Fun}(C, C)$$\mathrm{Fun}^L(C, D)$$(FG)^R = G^R F^R$$-^R$$-^R$$M$ with the structure of a monad, what you get out is a comonad.

By the way, this:

Let $(\times)$ be a product bifunctor in $C$. As $C$ is CCC, we can curry $(\times)$

is slightly incorrect. For one, the usual terminology would be (if I'm not mistaken) that $\times$ is a bifunctor over or on $C$. "In" typically means constructions using the arrows and objects of a category, whereas functors "on" categories refer to constructions relating multiple categories. And the product bifunctor isn't a construction within a Cartesian category.

And this relates to the larger inaccuracy: the ability to curry the product bifunctor has nothing to do with $C$ being Cartesian closed. Rather, it is possible because $Cat$, the category of categories (insert caveats) is Cartesian closed. So the currying in question is given by:

where $C \times D$ is a product of categories, and $E^D$ is the category of functors $F : D \to E$. This works regardless of whether $C$, $D$ and $E$ are Cartesian closed, though. When we let $C = D = E$, we get:

But this is merely a special case of:

Consider the adjunction $\langle F,G,\epsilon,\eta \rangle$. For every such adjunction we have a monad $\langle GF, \eta, G\epsilon F\rangle$ and also a comonad $\langle FG, \epsilon, F\eta G\rangle$. Notably, $F$ and $G$ need not be endofunctors, and in general they aren't (e.g., the list monad is an adjuction between the free and forgetful functors between $\mathbf{Set}$ and $\mathbf{Mon}$).

So, what you want to do is take Reader (or Writer) and decompose it into the adjoint functors which give rise to the monad and the corresponding comonad. Which is to say that the connection between Reader and Coreader (or Writer and Cowriter) isn't the one you're looking for.

And it's probably better to think of currying as $-^\ast : \text{hom}({-}\times A, {=}) \cong \text{hom}({-}, {=}^A)$, i.e. $\forall X,Y.~ \lbrace f : X\times A \to Y \rbrace \cong \lbrace f^\ast : X \to Y^A \rbrace$. Or if it helps, $-^\ast : \text{hom}({-}\times A, {=}\times 1) \cong \text{hom}({-}^1, {=}^A)$