nLab
writer comonad

Idea

In a cartesian closed category/type theory $\mathcal{C}$, given any object/type $W$ there is a comonad

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

given by forming the Cartesian product with $W$

If here $W$ is equipped with the structure of a monoid, then $W \times (-)$ also canonically inherits the structure of a monad (see writer monad).

In the context of monads in computer science this is called the writer monad. This is the case of interest in functional programming languages such as Haskell, where a program for the form $X \longrightarrow W \times Y$ behaves like a program taking input of type $X$ to output of type $Y$ while in addition producing output of type $W$, which is aggregated using the the monoid when the functions are composed, creating a sort of side channel.

Properties

Relation to reader monad and state monad

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

The composite of writer 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 writer 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 \,.$$

Related concepts

• writer monad

• maybe monad

• continuation monad

• reader monad, state monad

References

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

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