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 lens-data structures (O’Connor (2010), (2011); see there) used to inspect and edit fields (“views”) in databases.

## Definition

### On a cartesian closed category

By default, the costate comonad is understood to be defined on a cartesian closed category $(\mathcal{C}, \times \ast)$ whose internal hom we denote by $[\text{-}, \text{-}]$.

This means that given an object $S \in \mathcal{C}$ there is a pair of adjoint functors

(1)$\mathcal{C} \underoverset {\underset{[S,\text{-}]}{\longrightarrow}} {\overset{S \times (\text{-})}{\longleftarrow}} {\;\; \bot \;\;} \mathcal{C} \,.$

Notice that

• the unit of this adjunction (being the adjunct of the identity morphism on ${S \times D}$) is:

(2)$\array{ D & \overset{ ret^{ S State }_D }{\longrightarrow} & \big[ S ,\, S \times D \big] \\ d &\mapsto& \big( s \mapsto (s,d) \big) \mathrlap{\,,} }$
• the counit of this adjunction (being the adjunct of the identity morphism on ${[S,D]}$) is the evaluation map

(3)$\array{ S \times [S,D] & \overset{ obt^{S Store}_D }{\longrightarrow} & D \\ \big( s, f \big) &\mapsto& f(s) \mathrlap{\,.} }$

While the $S$-state monad is the monad induced by this adjunction (1)

$S State \,\coloneqq\, \big[ S ,\, S \times (\text{-}) \big]$

the $S$-state comonad is the induced comonad

$S Store \,\coloneqq\, S \times \big[ S,\, (\text{-}) \big] \,.$

whose counit is (3) and whose duplicate operation (comonad coproduct) is given by the unit (2) as

$\array{ S \times [S, D] & \overset{ S \times ret^{S State}_{[S,D]} } {\longrightarrow} & S \times \big[S, S \times [S,D] \big] \\ (s, f) &\mapsto& \Big( s ,\, \big( s' \,\mapsto\, (s', f) \big) \Big) }$

Therefore the comonadic extend operation sends a coKleisli morphism

$\mathcal{O} \,\colon\, S \times [S,D] \longrightarrow D'$

to

$\array{ \mathllap{ extend^{ S Store }_{D,D'} \mathcal{O} \;\;\colon\;\; } S \times [S,D] &\overset{ S \times ret^{S State}_{[S,D]} }{\longrightarrow}& S \times \big[ S \times [S,D] \big] &\overset{ S \times \big[ S, \mathcal{O} \big] }{\longrightarrow}& S \times [S, D'] \\ (s,f) &\mapsto& \Big( s ,\, \big( s' \,\mapsto\, (s', f) \big) \Big) &\mapsto& \Big( s ,\, \big( s' \,\mapsto\, \mathcal{O}(s',f) \big) \Big) \mathrlap{\,.} }$

In applications of comonads in computer science one thinks of

• $S$ as an address type,

• $[S,D]$ a data base of $S$-indexed $D$-data

hence of the $S Store$-comonad on $D$ as providing the computational context consisting of data base (of “stored $D$-values”, whence the name store comonad) and an address.

Thus the obtain-operation (3) literally obtains (reads, extracts) the memory content at the given address.

### On closed monoidal categories

More generally, for $(\mathcal{C}, \otimes, \mathbb{1})$ a closed monoidal category (not necessarily cartesian), every object $D$ still still gives an internal-hom adjunction of the form (1)

(4)$\mathcal{C} \underoverset {\underset{[S,\text{-}]}{\longrightarrow}} {\overset{S \otimes (\text{-})}{\longleftarrow}} {\;\; \bot \;\;} \mathcal{C}$

Particularly when $\mathcal{C} \,\equiv\, Mod_{\mathbb{C}}$ is the category of complex vector spaces (“$\mathbb{C}$-linear spaces”) this gives a linear form of the costate comonad, discussed at

## Properties

### Realization by base change

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.

### Store-Comodales are Lenses

We spell out the data of comodales over the classical Store-comonad (from above).

(Beware that we are switching herefrom using “$S$” for the state space to using it for the argument of the comonad – this in order to be closer to the notation used at lens in computer science.)

Unwinding the definitions, a $V$-store comodale structure on a type $S$ is a map of the form

(5)$\array{ S & \overset{ \big( get ,\, \widetilde{put} \big) }{\longrightarrow} & V \times [V, S] \\ s &\mapsto& \big( get(s) ,\, put(-,s) \big) }$

and hence consists, equivalently, of a pair of functions of the form

(6)$\begin{array}{l} get \;\colon\; S \to V \,, \\ put \;\colon\; V \times S \to S \,. \end{array}$

On this data, the counitality condition of a comodale (5) requires that the following composite is the identity

$\array{ S & \overset{ \big( get ,\, \widetilde{put} \big) }{\longrightarrow} & V \times [V, S] & \overset{ obt^{ V Store }_S \equiv ev }{\longrightarrow} & S \\ s &\mapsto& \big( get(s) ,\, put(-,s) \big) &\mapsto& put\big( get(s) ,\, s \big) \mathrlap{\,,} }$

hence that

(7)$s \in S \;\;\;\;\;\; \vdash \;\;\;\;\;\; put\big( get(s) ,\, s \big) \;=\; s \mathrlap{\,,}$

while the coaction property requires that the following diagram commutes

which amounts to the two conditions

(8)$v \in V ,\; s \in S \;\;\;\;\;\; \vdash \;\;\;\;\;\; get\big( put(v,s) \big) \,=\, v$

and

(9)$\label{} v, v' \in V ,\, s \in S \;\;\;\;\;\;\; \vdash \;\;\;\;\;\;\; put\big( v ,\, put(v', s) \big) \,=\, put(v,\, s)$

This data — a pair of maps (6) satisfying the get-put law (7), the put-get law (8) and the put-put law (9) – is known as a lawful lens in computer science (see there).

Hence, as first observed by O’Connor 2010:

###### Proposition

Classical $V$-store comodales are equivalently lawful lenses with “view” $V$.

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

Early review:

Further details:

Further review: