Lecteur, écrivain monades

Soit $C$ un CCC . Soit $(\times)$ être un bifoncteur produit sur $C$ . Comme Cat est CCC, nous pouvons curry $(\times)$ :

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

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

Catégorie de foncteurs $C \Rightarrow C$ a une structure monoïdale habituelle. A monoid en $C \Rightarrow C$ est une monade en $C$ . Nous considérons que les produits finis que la structure monoïdale sur $C$ .

$curry (\times) 1 \cong id$

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

Par conséquent préserve la structure monoïdale, donc il transporte un monoïde vers une monade et un comonoïde vers une comonade. À savoir, il transporte un monoïde arbitraire w vers ( W r i t e r w ) monade (regardez la définition - w doit être un monoïde). De même, il transporte la comonoïde diagonale vers la comonade Coreader.$(curry (\times))$$w$$(Writer\ w)$$w$

Maintenant, pour être concret, je déplie la construction de Writer.

Commencer. En fait , ils ont simplement des noms distincts dans Haskell. Nous avons une monoid Haskell ⟨ w , m a p p e n d , m e m p t y ⟩ :$Writer = Coreader = curry(\times)$ $\langle w, mappend, mempty\rangle$

$mappend : w\times w \to w$

$mempty : 1 \to w$

Writer est un foncteur, il doit donc cartographier également les morphismes, tels que et m e m p t y . J'écris ceci comme ci-dessous, bien qu'il ne soit pas valide dans Haskell:$mappend$$mempty$

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

est une transformation naturelle, un morphisme en C ⇒ C . Par propriétés de c $Writer\ mappend$$C\Rightarrow C$ c'est une fonction, qui prend a ∈ O b ( C ) et donne un morphisme en 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 façon informelle, des composants de leur montant de type p et pompes$Writer\ mappend\ a$$w$ intacte. C'est exactement la définition de Writer dans Haskell. Un obstacle est que pour la monade ⟨ W r i t e r w , μ , r | ⟩ nous avons besoin$a$$\langle Writer\ w,\mu,\eta\rangle$

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

c'est-à-dire incompatibilité des types. Mais ces foncteurs sont isomorphes: par l'associateur habituel pour les produits finis qui est un isomorphisme naturel ≅ λ 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$ . On définit alors via W r i t e r m $\mu$ . J'omets une construction de η via m e m p t y .$Writer\ mappend$$\eta$$mempty$

Écrivain, être un foncteur, conserve des diagrammes commutatives, à savoir les conserves monoid égalités, nous avons donc des égalités prouvé accordées pour = monoid dans ( C ⇒ C ) = une monade en C . Fin.$\langle Writer\ w,\mu,\eta\rangle$$(C\Rightarrow C)$$C$

Et Reader et Cowriter? Le lecteur est adjoint à Coreader, comme expliqué dans la définition de Coreader, voir le lien ci-dessus. De même, Cowriter est adjoint à Writer. Je n'ai pas trouvé de définition de Cowriter, je l'ai donc inventée par analogie dans le tableau:

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

Voici les définitions simplifiées de ces (co) monades. fr_ob F désigne une cartographie d'un foncteur F sur des objets, fr_mor F désigne une cartographie d'un foncteur F sur des morphismes. Il est un objet de monoid en C .$\langle w,\hat{+},\hat{0}\rangle$$C$

• Écrivain
  • $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$
• Lecteur
  • $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 question est que l'adjonction en concerne les foncteurs, pas les monades. Je ne vois pas comment l'adjonction implique "Coreader est une comonade" → "Reader est une monade" et "Writer est une monade" → "Cowriter est une comonade".$C$$\to$$\to$

Remarque. J'ai du mal à fournir plus de contexte. Cela demande du travail. Surtout, si vous avez besoin d'une pureté catégorique et que ces (co) monades ont été introduites pour les programmeurs. Continuez à harceler! ;)

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

$C$$D$$\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$.

If $C = D$, then $\mathrm{Fun}(C, C)$ has a monoidal structure given by composition and so does $\mathrm{Fun}^L(C, D)$, because the composition of left adjoints is a left adjoint. Specifically, $(FG)^R = G^R F^R$, so $-^R$ is an antimonoidal contravariant functor. If you apply $-^R$ to the structural natural transformations which equip a functor $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)$