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 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$-store 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}$$

and the induced monad and comonad may be understood as substructural forms of the state monad and store comonad, respectively.

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

• quantum costate comonad.

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-Comodules are Lenses

We spell out the data of comodules over the classical Store comonad defined above.

(Beware that we are switching from 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 comodule 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 comodule (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 comodules are equivalently lawful lenses with “view” $V$.

Related concepts

• quantum costate comonad

• maybe monad,

• continuation monad

• state monad

• function monad (reader monad)

References

General

• Bartosz Milewski (compiled by Igal Tabachnik), §23.6 in: Category Theory for Programmers, Blurb (2019) [pdf, github, webpage, ISBN:9780464243878]

• Tarmo Uustalu, slide 14 of: Monads and Interaction Lecture 3 , lecture notes for MGS 2021 (2021) [pdf, pdf]

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:

• 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)

• Bartosz Milewski, pp 240 in: The Dao of Functional Programming (2023) [pdf, github]