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}

Advertisements

6 Responses

Subscribe to comments with RSS.

  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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: