# reperiendi

## I finally understand the state transformer monad!

Posted in Category theory by Mike Stay on 2008 October 29

It’s the monad arising from the currying adjunction between $FX = X \times Y$ and $GZ = Y \multimap Z.$  $GF$ attaches an environment $Y$ to $X$:

$GFX = Y \multimap (X \times Y)$

This is the type of a function that takes a state of type $Y$ and outputs a result of type $X$ and a new state of type $Y$. So $G$ is the ability to depend on state and $F$ is the ability to change the state.

The natural transformation $\epsilon:FG \Rightarrow 1,$ is evaluation:

$\epsilon_X:(Y \multimap X) \times Y \to X$

takes a function and an input point and evaluates the function at that point.  So we get

$\mu:GFGF \Rightarrow GF$

by evaluating the $FG$ in the middle, while the unit

$\eta:1 \Rightarrow GF$

is just the curried identity on pairs:

$\begin{array}{rl}\eta_X:X & \to Y \multimap (X \times Y) \\ x & \mapsto \lambda y.(x,y)\end{array}$

### 6 Responses

1. jkb71 said, on 2009 September 21 at 2:20 am

I don’t understand the \multimap symbol. Do you mean that the type GZ is a function from Y returning multiple values in Z?

If so, does ‘multiple values’ equal ‘a subset of Z’?
Ummm… or perhaps ‘a finite subset of Z’?

2. reperiendi said, on 2009 October 11 at 2:37 pm

The lollipop (\multimap) is also used for linear implication in linear logic; in computer programming, they usually use the arrow (\to). So a function f taking a value of type A and returning a function from B to C is written

$f:A \to B \multimap C$

3. Avery D Andrews said, on 2011 July 30 at 8:22 pm

$\epsilon$ and $\eta$ seem to me to be reversed.

• reperiendi said, on 2011 July 30 at 8:38 pm

Reversed from what?

• Avery D Andrews said, on 2011 July 30 at 9:07 pm

$\epsilon$ and $\eta$ seem to me to be reversed

In my books and downloaded papers, $\eta$ goes from 1 to GF in the left-hand category, $\epsilon$ from FG to 1 on left, so that $\epsilon$ is evaluation and $\eta$ is ‘placeholder’, and also does what the state transformer monad unit is supposed to do.

• reperiendi said, on 2011 July 30 at 9:34 pm

OK, sure. I’ve changed them around now.