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$.
In the context of monads in computer science this is called the writer comonad. This is of interest in functional programming languages such as Haskell, where a program for the form $X \longrightarrow W \times Y$ behaves like taking input of type $X$ to output of type $Y$ while in addition producing output (βside effectβ) of type $W$.
If here $W$ is 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. (See writer monad.)
In a cartesian closed category/type theory $\mathcal{C}$, the writer comonad $W\times (-)$ is left adjoint to the reader monad $[W,-]$.
The composite of writer 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 writer 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
Last revised on March 13, 2021 at 03:53:07. See the history of this page for a list of all contributions to it.