Pembaca, Penulis monads

Biarkan menjadi CCC . Mari menjadi bifunctor produk pada . Karena Cat adalah CCC, kita dapat menjilat :$C$$(\times)$$C$$(\times)$

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

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

Kategori memiliki struktur monoid biasa. $C \Rightarrow C$ Sebuah monoid di adalah monad di . $C \Rightarrow C$$C$ Kami mempertimbangkan produk yang terbatas sebagai struktur monoidal di .$C$

$curry (\times) 1 \cong id$

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

Oleh karena itu mempertahankan struktur monoid, sehingga mengangkut monoid ke monad dan komonoid ke comonad. Yaitu, mengangkut sebuah monoid sewenang-wenang ke monad (lihat definisi - harus monoid a). Demikian pula itu mengangkut comonoid diagonal ke comonad Coreader.$(curry (\times))$$w$$(Writer\ w)$$w$

Sekarang, untuk konkret, saya membuka konstruksi Penulis.

Mulai. Sebenarnya , mereka hanya memiliki nama yang berbeda di Haskell. Kami memiliki monoid :$Writer = Coreader = curry(\times)$ $\langle w, mappend, mempty\rangle$

$mappend : w\times w \to w$

$mempty : 1 \to w$

Writer adalah functor, jadi ia harus memetakan juga morfisme, seperti dan . Saya menulis ini seperti di bawah ini, meskipun tidak valid di Haskell:$mappend$$mempty$

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

$Writer\ mappend$ adalah transformasi alami, morphism di . Dengan sifat itu adalah fungsi, yang mengambil dan memberikan morfisme dalam :$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$

Secara informal, menjumlahkan komponen tipe dan memompakan utuh. Ini persis definisi Writer di Haskell. Satu kendala adalah bahwa untuk monad kita butuhkan$Writer\ mappend\ a$$w$$a$$\langle Writer\ w,\mu,\eta\rangle$

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

yaitu ketidakcocokan jenis. Tetapi fungsi-fungsi ini isomorfis: oleh associator biasa untuk produk hingga yang merupakan isomorfisme alami . Kemudian kita mendefinisikan melalui . Saya menghilangkan konstruksi melalui .$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$$Writer\ mappend$$\eta$$mempty$

Writer, sebagai functor, mempertahankan diagram komutatif, yaitu mempertahankan persamaan monoid, jadi kami telah memberikan persamaan yang terbukti untuk = monoid dalam = sebuah monad di . Akhir.$\langle Writer\ w,\mu,\eta\rangle$$(C\Rightarrow C)$$C$

Bagaimana dengan Reader dan Cowriter? Pembaca disatukan dengan Coreader, seperti yang dijelaskan dalam definisi Coreader, lihat tautan di atas. Demikian pula, Cowriter adalah tambahan untuk Writer. Saya tidak menemukan definisi Cowriter, jadi saya mengarangnya dengan analogi seperti pada tabel:

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

Di bawah ini adalah definisi yang disederhanakan dari monad tersebut. fr_ob F menunjukkan pemetaan functor F pada objek, fr_mor F menunjukkan pemetaan functor F pada morfisme. Ada objek monoid di .$\langle w,\hat{+},\hat{0}\rangle$$C$

• Penulis
  • $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$
• Pembaca
  • $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$
• Penulis
  • $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)$

Pertanyaannya adalah bahwa tambahan di berhubungan dengan functors, bukan monads. Saya tidak melihat bagaimana susunannya menyiratkan "Coreader is a comonad" "Reader is a monad" dan "Writer is a monad" "Cowriter is a comonad".$C$$\to$$\to$

Ucapan. Saya berjuang untuk memberikan lebih banyak konteks. Itu membutuhkan pekerjaan. Terutama, jika Anda memerlukan kemurnian kategori dan mereka (co) monad diperkenalkan untuk programmer. Terus mengomel! ;)

Ya, jika monad memiliki adjoin kanan N , maka N secara otomatis mewarisi struktur comonad.$M : C \to C$$N$$N$

Pengaturan kategori-teori umum untuk memahami ini adalah sebagai berikut. Biarkan dan D menjadi dua kategori. Tulis F u n ( C , D ) untuk kategori fungsi dari C ke D ; Objek-objeknya adalah functors dan transformasi-transformasi morfismenya yang alami. Tulis F u n L ( C , D ) untuk subkategori lengkap F u n ( C , D $C$$D$$\mathrm{Fun}(C, D)$$C$$D$$\mathrm{Fun}^L(C, D)$$\mathrm{Fun}(C, D)$pada functors yang memiliki adjoin kanan (dengan kata lain, kami menganggap functors dengan adjoin kanan dan transformasi sewenang-wenang alami di antara mereka). Menulis untuk adjoint kanan functor . Kemudian adalah functor kontravarian: jika adalah transformasi alami maka ada diinduksi alami transformasi .$C \to D$$F^R : D \to C$$F : C \to D$$-^R : \mathrm{Fun}^L(C, D) \to \mathrm{Fun}(D, C)$$\alpha : F \to G$$\alpha^R : G^R \to F^R$

Jika , maka memiliki struktur monoid yang diberikan oleh komposisi dan demikian pula , karena komposisi adjoin kiri adalah adjoin kiri. Secara khusus, , jadi adalah functor kontravarian antimonoid. Jika Anda menerapkan pada transformasi alami struktural yang melengkapi fungsi dengan struktur monad, apa yang Anda dapatkan adalah sebuah comonad.$C = D$$\mathrm{Fun}(C, C)$$\mathrm{Fun}^L(C, D)$$(FG)^R = G^R F^R$$-^R$$-^R$$M$

Omong-omong, ini:

Mari menjadi bifunctor produk di C . Karena C adalah CCC, kita dapat menjilat ( × $(\times)$$C$$C$$(\times)$

sedikit salah. Untuk satu, terminologi biasa akan (jika saya tidak salah) yang adalah bifunctor lebih atau C . "In" biasanya berarti konstruksi yang menggunakan panah dan objek dari suatu kategori, sedangkan kategori functors "on" merujuk pada konstruksi yang berhubungan dengan banyak kategori. Dan bifunctor produk bukanlah konstruksi dalam kategori Cartesian.$\times$$C$

Dan ini berkaitan dengan ketidakakuratan yang lebih besar: kemampuan untuk menjilat produk bifunctor tidak ada hubungannya dengan karena Cartesian ditutup. Sebaliknya, itu mungkin karena C a t , kategori kategori (masukkan peringatan) adalah Cartesian ditutup. Jadi kari yang dimaksud diberikan oleh:$C$$Cat$

di mana adalah produk dari kategori, dan E D adalah kategori functors F : D → E . Ini berfungsi terlepas dari apakah C , D dan E tertutup Cartesian. Ketika kita membiarkan C = D = E , kita mendapatkan:$C \times D$$E^D$$F : D \to E$$C$$D$$E$$C = D = E$

c u r r y × : C → C

Tetapi ini hanyalah kasus khusus dari:

c u r r y F : C → E

$\langle F,G,\epsilon,\eta \rangle$$\langle GF, \eta, G\epsilon F\rangle$$\langle FG, \epsilon, F\eta G\rangle$$F$$G$$\mathbf{Set}$$\mathbf{Mon}$).

Jadi, apa yang ingin Anda lakukan adalah mengambil Reader (atau Writer) dan menguraikannya ke dalam adjoint functors yang menimbulkan monad dan comonad yang sesuai. Artinya, hubungan antara Reader dan Coreader (atau Writer dan Cowriter) bukan yang Anda cari.

$-^\ast : \text{hom}({-}\times A, {=}) \cong \text{hom}({-}, {=}^A)$$\forall X,Y.~ \lbrace f : X\times A \to Y \rbrace \cong \lbrace f^\ast : X \to Y^A \rbrace$$-^\ast : \text{hom}({-}\times A, {=}\times 1) \cong \text{hom}({-}^1, {=}^A)$