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
hom-set, hom-object, internal hom, exponential object, derived hom-space
loop space object, free loop space object, derived loop space
In a cartesian closed category/type theory $\mathcal{C}$, given any object/type $W$ there is a comonad
given by forming the Cartesian product with $W$, with the coproduct induced by the diagonal map on $W$ and the counit induced by the terminal map $W \to \ast$.
Notice then if $W$ is furthermore equipped with the structure of a monoid, then $W \times (-)$ also canonically inherits the structure of a monad, allowing aggregation of a programβs $W$ outputs, corresponding to a sort of side channel. Equipped with this monad-structure, the operation $W \times (-)$ is known as the writer monad, see there for more.
On the other hand, the canonical comonad structure on $W \times (-)$ is left adjoint to the reader monad, so that it is known as the reader comonad (eg. in the Haskell documentation for Control.Comonad.Reader) or coreader comonad (e.g. Ahman & Uustalu (2019)). It is also known as the product comonad (e.g. Uustalu & Vene 2008, p. 270).
In a cartesian closed category/type theory $\mathcal{C}$, the coreader comonad $W\times (-)$ is left adjoint to the reader monad $[W,-]$.
The composite of coreader comonad followed by reader monad is the state monad.
If the type system is even a locally Cartesian closed category/dependent type theory then for each type $W$ there is the base change adjoint triple
In terms of this then the coreader comonad is equivalently the composite
of context extension followed by dependent sum.
One may also think of this as being the integral transform through the span
(with trivial kernel) or as the polynomial functor associated with the span
Eg.
Danel Ahman, Tarmo Uustalu, p. 3 of: Decomposing Comonad Morphisms, CALCO 2019, Leibniz International Proceedings in Informatics (LIPIcs) 139 (2019) [doi:10.4230/LIPIcs.CALCO.2019.14]
Tarmo Uustalu, p. 13 of: Monads and Interaction Lecture 3, lecture notes for MGS 2021 (2021) [pdf, pdf]
Tarmo Uustalu, Varmo Vene, Comonadic Notions of Computation, Electronic Notes in Theoretical Computer Science 203 5 (2008) 263-284 [doi:10.1016/j.entcs.2008.05.029]
In Haskell:
See also:
Last revised on December 8, 2022 at 10:49:29. See the history of this page for a list of all contributions to it.