Monday, December 28, 2020

[jlylyjlr] not modifying state

import qualified Control.Monad.State as State;
import Control.Monad.State(State,runState);
type Mystate = ...

we can assert that a monadic function in the State monad does not modify state through comments:

-- f only reads state, and does not modify it.
f :: State Mystate Int;
f = ...

demo1 :: State Mystate ();
demo1 = do {
x <- f; -- f does not modify state

better would be to make the function pure, asserting it cannot modify state in a way the typechecker can verify:

f2 :: Mystate -> Int;
f2 = ...

demo2 :: State Mystate ();
demo2 = do {
x <- State.get >>= (return . f2);

the convenience function "gets" concisely enables the same thing:

demo3 :: State Mystate ();
demo3 = do {
x <- State.gets f2;

the name of "gets" suggests it is meant to be used for getting a projection of the state, using the specified projection function.  however, it can do any read-only computation on state, not limited to things which seem like projections.  (though arguably any read-only computation on state seems like a projection.)

originally, i thought we might have to do something much more complicated to assert at the type level that a function will not modify state, perhaps wrapping something with something using monad transformers Control.Monad.Reader.ReaderT or Control.Monad.State.StateT.  fortunately, nothing so complicated is needed.


the following is potentially confusing, so is not recommended for the faint of heart.  although we've made f2 above a pure function, we can still use monadic "do" notation to define it.  this is because a unary function is the Reader monad in disguise.  the "ask" or "get" function is "id".

{-# LANGUAGE ScopedTypeVariables #-}
astring :: Mystate -> String;
astring = do {
 foo :: Mystate <- id; -- read state
 return $ show foo;

f2 :: Mystate -> Int;
f2 = do {
 s1 :: String <- astring >>= doubleit >>= doubleit;
 return $ length s1;

-- monadic function that takes an argument.  the state variable should be the last input argument.
doubleit :: String -> Mystate -> String;
-- equivalently, read the above type signature as follows, where (->) is the type constructor for a read-only state monad, Mystate is encapsulated state, and String is the monadic return value.
doubleit :: String -> (((->) Mystate) String);
doubleit x = do {
 _ :: Mystate <- id; -- useless statement just to demonstrate reading state inside a do block
 return $ x++x;

No comments :