Contents

Examples

# Contents

## 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

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.

### General

(…)

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

Early review:

Further details:

Further review: