-- Haskell98!
-- | Variable state 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.
--
module Control.VarStateM where
import Control.Monad.State
-- | A parameterized `monad'
class Monadish m where
gret :: a -> m p p a
gbind :: m p q a -> (a -> m q r b) -> m p r b
-- | Inject regular monads to be monadish things too
newtype MW m p q a = MW{ unMW:: m a }
instance Monad m => Monadish (MW m) where
gret = MW . return
gbind (MW m) f = MW (m >>= unMW . f)
-- As a warm-up, we write the regular State computation, with the same
-- type of state throughout
-- | First, use the regular Monad.State
test1 = runState c (0::Int) where
c = do
v <- get
put (succ v)
return v
-- (0,1)
-- | Now, wrap in MW
test2 = runState (unMW c) (0::Int) where
c = gget `gbind` (
\v -> gput (succ v) `gbind` (
\_ -> gret v))
gget :: (MonadState s m) => MW m s s s
gget = MW get
gput :: (MonadState s m) => s -> MW m s s ()
gput = MW . put
-- (0,1)
-- | Introduce the variable-type state
--
newtype VST m si so v = VST{runVST:: si -> m (so,v)}
instance Monad m => Monadish (VST m) where
gret x = VST (\si -> return (si,x))
gbind (VST m) f = VST (\si -> m si >>= (\ (sm,x) -> runVST (f x) sm))
vsget :: Monad m => VST m si si si
vsget = VST (\si -> return (si,si))
vsput :: Monad m => so -> VST m si so ()
vsput x = VST (\si -> return (x,()))
-- Repeat test2 via VST: the type of the state is the same
test3 = runVST c (0::Int) >>= print where
c = vsget `gbind` (
\v -> vsput (succ v) `gbind` (
\_ -> gret v))
-- (1,0)
-- Now, we vary the type of the state, from Int to a Char
test4 = runVST c (0::Int) >>= print where
c = vsget `gbind` (
\v -> vsput ((toEnum (65+v))::Char) `gbind` (
\_ -> vsget `gbind` (
\v' -> gret (v,v'))))
-- ('A',(0,'A'))
{-
-- The following is an error:
Couldn't match `Char' against `Int'
Expected type: VST m Char r b
Inferred type: VST m Int Int Bool
test4' = runVST c (0::Int) >>= print where
c = vsget `gbind` (
\v -> vsput ((toEnum (65+v))::Char) `gbind` (
\_ -> vsget `gbind` (
\v' -> gret (v==v'))))
-}
-- | Try polymorphic recursion, over the state.
-- crec1 invokes itself, and changes the type of the state from
-- some si to Bool.
crec1 :: (Enum si, Monad m) => VST m si si Int
crec1 = vsget `gbind` (\s1 -> case fromEnum s1 of
0 -> gret 0
1 -> vsput (pred s1) `gbind` (\_ -> gret 1)
_ -> vsput True `gbind` (\_ ->
crec1 `gbind` (\v ->
(vsput s1 `gbind` -- restore state type to si
(\_ -> gret (v + 10))))))
test5 = runVST crec1 'a' >>= print
-- ('a',11)
-- | Another example, to illustrate locking and static reasoning about
-- the locking state
--
data Locked = Locked; data Unlocked = Unlocked
data LIO p q a = LIO{unLIO::IO a}
instance Monadish LIO where
gret = LIO . return
gbind m f = LIO (unLIO m >>= unLIO . f)
lput :: String -> LIO p p ()
lput = LIO . putStrLn
lget :: LIO p p String
lget = LIO getLine
-- In the real program, the following will execute actions to acquire
-- or release the lock. Here, we just print out our intentions.
lock :: LIO Unlocked Locked ()
lock = LIO (putStrLn "Lock")
unlock :: LIO Locked Unlocked ()
unlock = LIO (putStrLn "UnLock")
-- User code
tlock1 = lget `gbind` (\l ->
gret (read l) `gbind` (\x ->
lput (show (x+1))))
{-
*VarStateM> :t tlock1
tlock1 :: LIO p p ()
Inferred type has the same input and output states and is polymorphic:
tlock1 does not affect the state of the lock.
-}
tlock2 = lget `gbind` (\l ->
lock `gbind` (\_ ->
gret (read l) `gbind` (\x ->
lput (show (x+1)))))
{-
*VarStateM> :t tlock2
tlock2 :: LIO Unlocked Locked ()
The inferred type says that the computation does the locking.
-}
tlock3 = tlock2 `gbind` (\_ -> unlock)
{-
*VarStateM> :t tlock3
tlock3 :: LIO Unlocked Unlocked ()
-}
-- An attempt to execute the following
-- tlock4 = tlock2 `gbind` (\_ -> tlock2)
{-
gives a type error:
Couldn't match expected type `Locked'
against inferred type `Unlocked'
Expected type: LIO Locked r b
Inferred type: LIO Unlocked Locked ()
In the expression: tlock2
In a lambda abstraction: \ _ -> tlock2
The error message correctly points out an error of acquiring an already
held lock.
-}
-- Similarly, the following gives a type error because of an attempt
-- to release a lock twice
-- tlock4' = tlock2 `gbind` (\_ -> unlock `gbind` (\_ -> unlock))