Variable state monad
http://okmij.org/ftp/Computation/monads.html#param-monad
The familiar State monad lets us represent computations with a state that can be queried and
updated. The state must have the same type during the entire computation however. One sometimes
wants to express a computation where not only the value but also the type of the state can be
updated -- while maintaining static typing. We wish for a parameterized monad
that indexes each
monadic type by an initial (type)state and a final (type)state. The effect of an effectful
computation thus becomes apparent in the type of the computation, and so can be statically
reasoned about.
- class Monadish m where
- newtype MW m p q a = MW {
- unMW :: m a
- newtype VST m si so v = VST {
- runVST :: si -> m (so, v)
- vsget :: Monad m => VST m si si si
- vsput :: Monad m => so -> VST m si so ()
- crec1 :: (Enum si, Monad m) => VST m si si Int
- data Locked = Locked
- data Unlocked = Unlocked
- data LIO p q a = LIO {}
- lput :: String -> LIO p p ()
- lget :: LIO p p String
- lock :: LIO Unlocked Locked ()
- unlock :: LIO Locked Unlocked ()
Documentation
A parameterized monad
Inject regular monads to be monadish things too
First, use the regular Monad.State
Now, wrap in MW
Introduce the variable-type state
crec1 :: (Enum si, Monad m) => VST m si si IntSource
Try polymorphic recursion, over the state. crec1 invokes itself, and changes the type of the state from some si to Bool.
Another example, to illustrate locking and static reasoning about the locking state