Reasoning on State monad and unwrapping of do notation

[leadermaxone]

In my journey to understand the State monad I decided to try and unwrap the do notation into a series of binds (>>=) and subsequently apply the bind definition to further understand how the value and the state in a State monad are carried on between bound computations.

This post is intended as a way to confirm what I think happens and to correct my thoughts in case I understood it wrong.

Anyways, here is the starting snippet runState (do { cur<- getState; putState(cur+1) ; return "a" }) 34 which results in ("a", 35)

I copy here also the useful definitions.

data State s a = State {runState :: s -> (a, s)}

instance Monad (State s) where
    return = pure
    sa >>= f = State $ \s -> 
        let (a, s') = runState sa s
            sb = f a
            (b, s'') = runState sb s'  
            in (b, s'')

getState :: State s s 
getState = State $ \s -> (s, s)

putState :: s -> State s ()
putState new = State $ \_ -> ( (), new)

From the bind (>>=) implementation it is pretty clear how the value a is transmitted to the function f, what is not so clear is how the state s is carried as well and how modifications to it (like the ones made by putState) are executed and persisted. Or at least, it wasn't for me.

First step is to translate the do notation into a series of binds runState ( getState >>= (\cur -> putState (cur+1) >>=(\_-> return ("a"))) ) 34

Let's call State a the result of all the computation inside runState's argument State a = getState >>= (\cur -> putState (cur+1) >>=(\_-> return ("a")))

We know that State a will be a state that when run will return a function which will take a state (34 in this case) and return a tuple (value, newState).

Applying the definition of bind to State a we get this

State a = State $ \34 ->
    let (34, 34) = runState getState 34
        b = f 34
        (b, s'') = runState b 34
        in (b, s'')

getState returns a tuple with the state given to it both as value and newState, that's why I already "executed" it. As per definition the value (34) will be fed to f, the newState (34) will be fed to b when running it.

What is f? b = f 34 = (\34 -> putState (34+1) >>=(\_-> return ("a"))) it will return the State b, that once run will return a function which will expect an s and give back a tuple

Unwrapping once again what is happening in f..

State b = State $ (\s -> 
   let (v,s’) = runState (putState (34+1)) s
          c = f2 v
         (v’,s’’) = runState c s’
         in (v’,s’’)

again, what's f2? f2= (\_-> return ("a"))

Notice that the lambda discards the argument because in the do notation a line without the "var<-" part corresponds to (>>) which translates to ... >>= (_ -> ...)

return ("a") is immediate from the definition. I call the result State c. State c = State (\s -> ("a" , s))

Now we can start to go upwards. We know that "c = f2 v" is State c, that when run will take a state and return a tuple with "a" as value and a newState. Remember also that the result of putState is discarding whatever s it receives and putting its argument as the new state, () as the value.

State b = State $ (\s -> 
    let ((),35) = runState (putState (34+1)) s -- s is ignored by putState
               c = State (\s -> ("a" , s) -- f2 ()
               ("a",35) = runState c 35
               in ("a",35)

As per (>>=) definition, c will be run with the state resulting from running putState, which is 35. the value "()" is discarded in favor of "a" by f2

The result appears to be already there, but how is it transferred towards outer functions?

Now that we know what State b is let's substitute it

State a = State $ \34 ->
    let (34, 34) = runState getState 34
        b = State (\s -> ("a", 35)
        ("a", 35) = runState b 34
        in ("a", 35)

Since putState ignored the s in favor of 35, and return only concerned itself with the value "a", state b will always be a function giving back the tuple ("a", 35) in response to whatever s we throw at her. this means that runState b 34 is ("a", 35), and that's the result of running State a.

The complete (not executable) unwrapping is attached, rename it as .hs and use a wide monitor if possible. stateExe2.txt

Again, this is just the transcription of my reasoning, so that you can correct me if i'm wrong and stop my nightmares. Please.