nLab coreader comonad

Definition

Given an object $W$ in a category $\mathcal{C}$, if all binary cartesian products with $W$ exist, then taking the cartesian product with $W$ assembles into a comonad

$$W \times (-) \;\colon\; \mathcal{C} \longrightarrow \mathcal{C}$$

whose comultiplication is induced by the diagonal map on $W$ and whose counit is induced by the terminal map $W \to \ast$.

When $W$ is furthermore equipped with the structure of a monoid, then $W \times (-)$ also canonically inherits the structure of a monad. (Regarded as a monad in computer science this models the aggregation of a program’s $W$-typed outputs, corresponding to a sort of side channel.) Equipped with this monad-structure, the operation $W \times (-)$ is known as the writer monad, see there for more.

On the other hand, if $W$ is further exponentiable then $W \times (-)$ is left adjoint to the reader monad $W \to -$, so that it is known as the reader comonad (eg. in the Haskell documentation for Control.Comonad.Reader) or coreader comonad (e.g. Ahman & Uustalu (2019)). It is also known as the product comonad (e.g. Uustalu & Vene 2008, p. 270) and the environment comonad (eg. in the Haskell documentation for Control.Comonad.Env).

Coreader comonads in $\mathcal{C}^op$ are exception monads in $\mathcal{C}$, because products turn into coproducts.

Properties

As an indexed comonad

If all binary cartesian products in $C$ exist, then the coreader comonad extends to a $C$-indexed comonad on $C$, i.e. a functor $C \to Comonad$. If $C$ has a terminal object $1$, then the environment comonad $1 \times -$ is isomorphic to the identity comonad.

Generalization to tensor products

If $C$ is a monoidal category rather than having all binary products, then tensoring with an object $\Gamma \otimes -$ can be given an analogous comonad structure when $\Gamma$ has a comonoid structure. In a cartesian monoidal category every object has a unique comonoid structure, which is what induces the coreader comonad. Even without assuming objects carry comonoid structures, the action sending $\Gamma$ to the functor $\Gamma \otimes -$ defines a strong monoidal functor from $C$ to the monoidal category of endofunctors $[C,C]$, a degenerate kind of graded comonad.

Relation to reader monad and state monad

In a cartesian closed category/type theory $\mathcal{C}$, the coreader comonad $W\times (-)$ is left adjoint to the reader monad $[W,-]$.

The composite of coreader comonad followed by reader monad is the state monad.

In terms of dependent type theory

If the type system is even a locally Cartesian closed category/dependent type theory then for each type $W$ there is the base change adjoint triple

$$\mathcal{C}_{/W} \stackrel{\overset{\sum_W}{\longrightarrow}}{\stackrel{\overset{W^\ast}{\longleftarrow}}{\underset{\prod_W}{\longrightarrow}}} \mathcal{C}$$

In terms of this then the coreader comonad is equivalently the composite

$$\sum_W W^\ast = W\times (-) \;\colon\; \mathcal{C} \longrightarrow \mathcal{C}$$

of context extension followed by dependent sum.

One may also think of this as being the integral transform through the span

$$\ast \leftarrow W \rightarrow \ast$$

(with trivial kernel) or as the polynomial functor associated with the span

$$\ast \leftarrow W \stackrel{id}{\rightarrow} W \rightarrow \ast \,.$$

Coalgebras

A coalgebra of the coreader comonad $W \times -$ is equivalent to simply a morphism $A \to W$ for $A$ the carrier of the co-algebra. Furthermore, the category of coalgebras is the isomorphic to the slice category over $W$. This shows that if all cartesian products with $W$ exist, then the forgetful functor $\Sigma_W \colon C / W \to C$ is comonadic.

Related concepts

(co)monad name	underlying endofunctor	(co)monad structure induced by
reader monad	$W \to (\text{-})$ on cartesian types	unique comonoid structure on $W$
coreader comonad	$W \times (\text{-})$ on cartesian types	unique comonoid structure on $W$
writer monad	$A \otimes (\text{-})$ on monoidal types	chosen monoid structure on $A$
cowriter comonad	$\array{A \to (\text{-}) \\ \\ A \otimes (\text{-})}$ on monoidal types	chosen monoid structure on $A$ chosen comonoid structure on $A$
Frobenius (co)writer	$\array{A \to (\text{-}) \\ A \otimes (\text{-})}$ on monoidal types	chosen Frobenius monoid structure

• maybe monad

• continuation monad

• state monad

• exception monad

References

Eg.

• Danel Ahman, Tarmo Uustalu, p. 3 of: Decomposing Comonad Morphisms, CALCO 2019, Leibniz International Proceedings in Informatics (LIPIcs) 139 (2019) [doi:10.4230/LIPIcs.CALCO.2019.14]

• Tarmo Uustalu, p. 13 of: Monads and Interaction Lecture 3, lecture notes for MGS 2021 (2021) [pdf, pdf]

• Tarmo Uustalu, Varmo Vene, Comonadic Notions of Computation, Electronic Notes in Theoretical Computer Science 203 5 (2008) 263-284 [doi:10.1016/j.entcs.2008.05.029]

In Haskell:

• Control.Comonad.Reader

See also:

• Philip Wadler, The essence of functional programming, 1992.

• Olivier Verdier, The Reader and Writer Monads and Comonads, 2014