natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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.
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
Notice that
the unit of this adjunction (being the adjunct of the identity morphism on ${S \times D}$) is:
the counit of this adjunction (being the adjunct of the identity morphism on ${[S,D]}$) is the evaluation map
While the $S$-state monad is the monad induced by this adjunction (1)
the $S$-store comonad is the induced comonad
whose counit is (3) and whose duplicate operation (comonad coproduct) is given by the unit (2) as
Therefore the comonadic extend operation sends a coKleisli morphism
to
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.
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)
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
In a locally Cartesian closed category/dependent type theory $\mathbf{H}$, then to every type $W$ is associated its base change adjoint triple
In terms of this the store comonad is the composite
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.
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
and hence consists, equivalently, of a pair of functions of the form
On this data, the counitality condition of a comodule (5) requires that the following composite is the identity
hence that
while the coaction property requires that the following diagram commutes
which amounts to the two conditions
and
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 $V$-store comodules are equivalently lawful lenses with “view” $V$.
function monad (reader monad)
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]
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:
Further details:
Further review:
Bartosz Milewski, pp 240 in: The Dao of Functional Programming (2023) [pdf, github]
Last revised on January 24, 2024 at 03:14:22. See the history of this page for a list of all contributions to it.