nLab store comonad

Idea

The store comonad (also costate comonad, as it is left adjoint to the state monad) is a co-monad (in computer science) used to implement computational storage and retrieval of data (databases) in functional programming.

Concretely, the coalgebras over the store monad are equivalently the well-behaved lense-data structures (O’Connor (2010), (2011); see there) used to inspect and edit fields (“views”) in databases.

Definition

On a cartesian closed category, the costate comonad is that induced by the internal hom-adjunction (left adjoint to the state monad).

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

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

with natural transformations the counit,

$$\varepsilon : D X \rightarrow X$$

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

usually called extract and comultiplication,

$$\delta: D X \rightarrow D D X$$

$$\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.

Related concepts

• maybe monad,

• continuation monad

• state monad

• function monad (reader monad)

References

General

(…)

Related to lenses

The observation that lenses (in computer science) are equivalently the coalgebras of the costate comonad (cf. monads in computer science) is due to:

• Russell O’Connor, Lenses Are Exactly the Coalgebras for the Store Comonad (30th Nov 2010) [r6research:23705]

• Russell O'Connor, Functor is to Lens as Applicative is to Biplate: Introducing Multiplate, contribution to ICFP ‘11: ACM SIGPLAN International Conference on Functional Programming (2011) [arXiv:1103.2841]

Early review:

• Jeremy Gibbons, Lenses are the coalgebras for the costate comonad (2011)

Further details:

• Jeremy Gibbons, Michael Johnson, Relating Algebraic and Coalgebraic Descriptions of Lenses, Electronic Communications of the EASST 49 (2012) [doi:10.14279/tuj.eceasst.49.726, pdf]

Further review:

• Bartosz Milewski, Lenses, Stores, and Yoneda (2013)