State is a Monad

[sassa_nf]

The proof: https://math.stackexchange.com/a/4250143

It's kind of funny how the proof becomes trivial, if you express the types the right way.

Comments

[chaource]

I found a very simple proof that State is a monad, that makes it visually clear.


We will prove that State is a monad if we prove that the Kleisli arrows compose associatively and with unit.

kleisli arrow for State is of type a -> State b, which is the same as a -> s -> (s, b)

Uncurry and flip arguments, and obtain an equivalent type : (s, a) -> (s, b)

then show that the Kleisli composition for State is the same as the ordinary composition for functions of type (s, a) -> (s, b)

also prove that the unit is the identity function of type : (s, a) -> (s, a)

And that’s it.