Czytnik, pisarz monady

Niech będzie CCC . Niech być bifunctor produkt na . Ponieważ Cat to CCC, możemy curry :( × ) C ( × $C$$(\times)$$C$$(\times)$

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

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

Kategoria funktora ma zwykłą strukturę monoidalną. $C \Rightarrow C$ Monoid w jest monada w . $C \Rightarrow C$$C$ Uważamy produktów skończonych jak monoidal struktury na .$C$

$curry (\times) 1 \cong id$

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

Dlatego zachowuje strukturę monoidalną, więc transportuje monoid do monady, a comonoid do comonady. Mianowicie, przenosi ona dowolną monoidę do monady (spójrz na definicję - musi być monoidą). Podobnie przenosi diagonalny comonoid do comonada Coreadera.$(curry (\times))$$w$$(Writer\ w)$$w$

Teraz, dla konkretności, rozwijam konstrukcję Writer.

Zaczynać. W rzeczywistości , po prostu mają różne nazwy w Haskell. Mamy monoid Haskella :$Writer = Coreader = curry(\times)$ $\langle w, mappend, mempty\rangle$

$mappend : w\times w \to w$

$mempty : 1 \to w$

Writer jest funktorem, więc musi mapować także morfizmy, takie jak i . Piszę to jak poniżej, choć jest to nieprawidłowe w Haskell:$mappend$$mempty$

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

$Writer\ mappend$ naturalna transformacja, morfizmem w . Według właściwości jest to funkcja, która przyjmuje i daje morfizm w :$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$

Nieformalnie, sumuje elementy typu i pompy nienaruszone. To jest dokładnie definicja Writer w Haskell. Jedną przeszkodą jest to, że dla monad potrzebujemyw ⟨ W r i t e r w , μ , r | $Writer\ mappend\ a$$w$$a$$\langle Writer\ w,\mu,\eta\rangle$

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

tj. niezgodność typów. Ale te funktory są izomorficzne: przez zwykłego asocjatora dla produktów skończonych, który jest naturalnym izomorfizmem . Następnie definiujemy przez . Pomijam budowę przez .≅ λ a . w × ( w × a ) = W r i t e r w ∘ W r i t e r w μ W r i t e r m a p p $Writer (w\times w) = \lambda a. (w\times w)\times a$$\cong \lambda a. w\times(w\times a) = Writer\ w \circ Writer\ w$$\mu$η m e m p t $Writer\ mappend$$\eta$$mempty$

Writer, będący funktorem, zachowuje diagramy przemienne, tzn. Zachowuje równości monoidów, więc z góry udowodniliśmy równości dla = monoid w = monada w . Koniec.( C ⇒ C ) $\langle Writer\ w,\mu,\eta\rangle$$(C\Rightarrow C)$$C$

Co z Czytelnikiem i Cowriter? Czytelnik jest połączony z Coreaderem, jak wyjaśniono w definicji Coreadera, patrz link powyżej. Podobnie Cowriter przylega do Writer. Nie znalazłem definicji Cowriter, więc wymyśliłem ją przez analogię pokazaną w tabeli:

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

Poniżej znajdują się uproszczone definicje tych (ko) monad. fr_ob F oznacza odwzorowanie funktora F na obiektach, fr_mor F oznacza odwzorowanie funktora F na morfizmach. Jest to obiekt monoid w .$\langle w,\hat{+},\hat{0}\rangle$$C$

• Pisarz
  • $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$
• Czytelnik
  • $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)$

Pytanie brzmi, że dodatek w dotyczy funktorów, a nie monad. Nie rozumiem, jak to powiązanie sugeruje, że „Coreader to comonada” „Reader to monada”, a „Writer to monada” „Cowriter to comonada”.$C$$\to$$\to$

Uwaga. Usiłuję zapewnić więcej kontekstu. Wymaga trochę pracy. Zwłaszcza jeśli potrzebujesz jakościowej czystości, a te (ko) monady zostały wprowadzone dla programistów. Nie przestawaj dokuczać! ;)

Tak, jeśli monada ma prawe przyłączenie , wówczas automatycznie dziedziczy strukturę comonad.$M : C \to C$$N$$N$

Ogólne ustawienie teoretyczne kategorii, aby to zrozumieć, jest następujące. Niech i będą dwiema kategoriami. Napisz dla strategii funktorów od do ; Jego obiektami są funktory, a morfizmy naturalne przekształcenia. Napisz$C$$D$$\mathrm{Fun}(C, D)$$C$$D$$\mathrm{Fun}^L(C, D)$$\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)$, 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)$