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 state monad is a monad (in computer science) used to implement computational side-effects in functional programming.
A functional program with input of type $X$, output of type $Y$ and mutable state type $W$ is a function (morphism) of type $X \times W \longrightarrow Y \times W$.
Under the (Cartesian product $\dashv$ internal hom)-adjunction this is equivalently given by its adjunct, which is a function of type
Here the operation $[W, W\times (-)]$ is the monad on the type system which is induced by the above adjunction; and this latter function is naturally regarded as a morphism in the Kleisli category of this monad.
In the context of monads in computer science, this monad $[W, W\times (-)] \colon \mathbf{H} \to \mathbf{H}$ is called the state monad for mutable states of type $W$.
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 state monad is the composite
of context extension followed by dependent sum, followed by context extension, followed by dependent product.
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.
function monad (reader monad)
Last revised on March 10, 2019 at 23:32:06. See the history of this page for a list of all contributions to it.