nLab
store comonad

Idea

The store comonad (also costate comonad) is a comonad (in computer science) used to implement computational storage and retrieval of data in functional programming.

As a comonadic triple $(D,\varepsilon,\delta)$ it is given by an endofunctor,

$$DX : X \rightarrow W \times [W,X],$$

with natural transformations the counit,

$$\varepsilon : DX \rightarrow Id_X$$

$$\varepsilon(v,f) \mapsto f(v),$$

usually called extract and comultiplication,

$$\delta: DX \rightarrow DDX$$

$$\delta (s, v) \mapsto (s, \lambda s' . (s', v)),$$

simply called duplicate.

Properties

Realization in dependent type theory

In a locally Cartesian closed category/dependent type theory $\mathbf{H}$, then to every type $W$ is associated its base change adjoint triple

$$\mathbf{H}_{/W} \stackrel{\overset{\sum_W}{\longrightarrow}}{\stackrel{\overset{W^\ast}{\longleftarrow}}{\underset{\prod_W}{\longrightarrow}}} \mathbf{H} \,.$$

In terms of this the store comonad is the composite

$$Store = \sum_W W^\ast \prod_W W^\ast$$

of context extension, followed by dependent product , followed by context extension, followed by dependent sum.

Here $\prod_W W^\ast = [W,-]$ is called the function monad or reader monad and $\sum_W W^\ast = W \times (-)$ is the writer comonad.

Reference

• Bartosz Milewski, Lenses, Stores, and Yoneda

• Jeremy Gibbons, Lenses are the coalgebras for the costate comonad

Related concepts

• maybe monad,

• continuation monad

• state monad

• function monad (reader monad)