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$
If here $W$ is equipped with the structure of a monoid, then $W \times (-)$ also canonically inherits the structure of a monad (see writer monad).
In the context of monads in computer science this is called the writer monad. This is the case of interest in functional programming languages such as Haskell, where a program for the form $X \longrightarrow W \times Y$ behaves like a program taking input of type $X$ to output of type $Y$ while in addition producing output of type $W$, which is aggregated using the the monoid when the functions are composed, creating a sort of side channel.
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 January 21, 2020 at 23:35:32. See the history of this page for a list of all contributions to it.