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 lense-data structures (O’Connor (2010), (2011); see there) used to inspect and edit fields (“views”) in databases.
On a cartesian closed category, the costate comonad is that induced by the internal hom-adjunction (left adjoint to the state monad).
In detail: As a comonadic triple it is given by an endofunctor,
with natural transformations the counit,
usually called extract and comultiplication,
simply called duplicate.
In a locally Cartesian closed category/dependent type theory , then to every type 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 is called the function monad or reader monad and is the writer comonad.
function monad (reader monad)
(…)
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:
Last revised on November 5, 2022 at 10:40:12. See the history of this page for a list of all contributions to it.