Contents

Examples

# Contents

## Idea

The state monad is a monad (in computer science) used to implement computational side-effects in functional programming.

A functional program with

1. input of (data-)type $X$,

2. output of type $Y$

3. and “mutable state” of type $W$

(e.g. the state of a “random access memory” device, cf. Yates (2019), p. 26 & Fig. 1.10)

is clearly a function (morphism) of function type betwen the product types with $W$:

$prog \;\colon\; X \times W \longrightarrow Y \times W \,.$

Now, under the hom-isomorphism of the (Cartesian product $\dashv$ internal hom)-adjunction, this is equivalently given by its adjunct, which is a function into the function type $[-,-]$ (internal hom):

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

The abstract notion of the state monad:

Concrete applications via implementation in Haskell:

Lecture notes:

In the generality of the local state monad: