nLab store comonad



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Modalities, Closure and Reflection



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.


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𝒞S \in \mathcal{C} there is a pair of adjoint functors

(1)𝒞[S,-]S×(-)𝒞. \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×D{S \times D}) is:

    (2)D ret D SState [S,S×D] d (s(s,d)), \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]{[S,D]}) is the evaluation map

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

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

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

the SS-store comonad is the induced comonad

SStoreS×[S,(-)]. 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

S×[S,D] S×ret [S,D] SState S×[S,S×[S,D]] (s,f) (s,(s(s,f))) \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

𝒪:S×[S,D]D \mathcal{O} \,\colon\, S \times [S,D] \longrightarrow D'


extend D,D SStore𝒪:S×[S,D] S×ret [S,D] SState S×[S×[S,D]] S×[S,𝒪] S×[S,D] (s,f) (s,(s(s,f))) (s,(s𝒪(s,f))). \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

  • SS as an address type,

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

hence of the SStoreS Store-comonad on DD as providing the computational context consisting of data base (of “stored DD-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 DD still still gives an internal-hom adjunction of the form (1)

(4)𝒞[S,-]S(-)𝒞 \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 𝒞Mod \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


Realization by base change

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

H /W WW * WH. \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= WW * WW * 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 WW *=[W,]\prod_W W^\ast = [W,-] is called the function monad or reader monad and WW *=W×()\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 “SS” 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 VV-store comodule structure on a type SS is a map of the form

(5)S (get,put˜) V×[V,S] s (get(s),put(,s)) \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)get:SV, put:V×SS. \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

S (get,put˜) V×[V,S] obt S VStoreev S s (get(s),put(,s)) put(get(s),s), \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)sSput(get(s),s)=s, 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)vV,sSget(put(v,s))=v v \in V ,\; s \in S \;\;\;\;\;\; \vdash \;\;\;\;\;\; get\big( put(v,s) \big) \,=\, v


(9)labelv,vV,sSput(v,put(v,s))=put(v,s) \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:


Classical VV-store comodules are equivalently lawful lenses with “view” VV.



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:

Last revised on January 24, 2024 at 03:14:22. See the history of this page for a list of all contributions to it.