ncatlab.org

store comonad in nLab

Contents

Context

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

homotopy levels

semantics

Modalities, Closure and Reflection

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∈𝒞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

SStore≔S×[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'

to

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

Properties

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⟶∏ W⟵W *⟶∑ 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:S→V, put:V×S→S. \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 VStore≡ev 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)s∈S⊢put(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)v∈V,s∈S⊢get(put(v,s))=v v \in V ,\; s \in S \;\;\;\;\;\; \vdash \;\;\;\;\;\; get\big( put(v,s) \big) \,=\, v

and

(9)labelv,v′∈V,s∈S⊢put(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:

References

General

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.