Contents

Contents

Idea

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

$X \longrightarrow [W, W \times Y ] \,.$

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$.

Properties

Realization in dependent type theory

In a locally Cartesian closed category/dependent type theory $\mathbf{H}$, then to every type $W$ is associated its base change adjoint triple

$\mathbf{H}_{/W} \stackrel{\overset{\sum_W}{\longrightarrow}}{\stackrel{\overset{W^\ast}{\longleftarrow}}{\underset{\prod_W}{\longrightarrow}}} \mathbf{H} \,.$

In terms of this the state monad is the composite

$State = \prod_W W^\ast \sum_W W^\ast$

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.

Last revised on March 10, 2019 at 23:32:06. See the history of this page for a list of all contributions to it.