Implementing the State Monad as a term algebra

# Documentation

Monadic actions are terms composed from the following constructors

Bind t f |

class RunBind t s a => RunState t s a | t s -> a whereSource

examples of terms

An example of an ill-formed term

An example of an ill-typed term The following term is ill-typed because it attempts to store both a boolean and a character in the state. Our state can have only one type.

The interpreter of monadic actions
It takes the term `t`

and the initial state of the type `s`

and returns the final state and the resulting value. The type
of the result, `a`

, is uniquely determined by the term and the state

class RunBind m s a whereSource

Interpretation of the Bind action requires an auxiliary class This is due to the polymorphism of the monadic bind, which has the type

m a -> (a -> m b) -> m b

Note the polymorphism both in `a`

(value type of the input monadic
action) and `b`

(value type of the resulting action)

We can now run (interpret) our sample terms

term2 denoted the action of negating the current state and returning the original state

Now, we show that our term representation of the state monad is an instance of MonadState