{-# OPTIONS -fglasgow-exts #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Implementing the State Monad as a term algebra
--
-- <http://okmij.org/ftp/Haskell/types.html#state-algebra>
--
module Control.StateAlgebra where

import Control.Monad
import Control.Monad.State hiding (runState)

-- | Monadic actions are terms composed from the following constructors
--
data Bind t f   = Bind t f
data Return v   = Return v
data Get        = Get
data Put v      = Put v

-- | examples of terms
term1 = (Return True) `Bind` Put
term2 = Get `Bind` (\v -> Put (not v) `Bind` (\() -> Return v))

-- | An example of an ill-formed term
term_ill1 = Get `Bind` Get
-- | 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.
term_ill2 = Put True `Bind` (\() -> Put 'a')


-- | 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 t s a => RunState t s a | t s -> a where
    runst :: t -> s -> (s,a)


instance RunState (Return a) s a where
    runst (Return a) s = (s,a)
instance RunState Get s s where
    runst _ s = (s,s)
instance RunState (Put s) s () where
    runst (Put s) _ = (s,())
instance (RunState m s a, RunState t s b)
    => RunState (Bind m (a->t)) s b where
    runst (Bind m k) s = runbind m k s

-- | 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)
--
class RunBind m s a where
    runbind :: RunState t s b => m -> (a->t) -> s -> (s,b)

instance RunBind (Return a) s a where
    runbind (Return a) k s = runst (k a) s

instance RunBind (Get) s s where
    runbind Get k s = runst (k s) s

instance RunBind (Put s) s () where
    runbind (Put s) k _ = runst (k ()) s

instance (RunBind m s x, RunState y s w)
    => RunBind (Bind m (x->y)) s w where
    runbind (Bind m f) k s
        = runbind m (\x -> Bind (f x) k) s

-- | We can now run (interpret) our sample terms
--
eterm1 = runst term1 False
-- (True,())

-- | term2 denoted the action of negating the current state and returning
-- the original state
eterm2 = runst term2 False
-- (True,False)

-- eterm_ill1 = runst term_ill1 True
-- The above gives an error message saying there is no rule
-- to interpret (Bind Get Get)
-- Indeed, this term is ill-formed.

-- eterm_ill2 = runst term_ill2 True
-- The error message says there is no rule (RunState (Put Char) Bool a)
-- That is, one can't store a Char in the state of the type Bool.
-- The above term is ill-typed indeed.


-- | Now, we show that our term representation of the state monad 
-- is an instance of MonadState
data Statte s a = forall t. RunState t s a => Statte t

instance RunState (Statte s a) s a where
    runst (Statte t) s = runst t s

instance RunBind (Statte s a) s a where
    runbind (Statte m) k s = runbind m k s

instance Monad (Statte s) where
    (Statte m) >>= f = Statte (Bind m (\x -> f x))
    return = Statte . Return

instance MonadState s (Statte s) where
    get = Statte Get
    put = Statte . Put

-- | We can write computations expressed by term1 and term2 using
-- the normal monadic syntax
--
-- The following identity function is to resolve polymorphism, to tell
-- that monadic terms below should use our representation of MonadState
as_statte :: Statte s a -> Statte s a
as_statte = id

-- term1 = (Return True) `Bind` Put
mterm1 = as_statte (return True >>= put)
emterm1 = runst mterm1 False
-- (True,())


-- term2 = Get `Bind` (\v -> Put (not v) `Bind` (\() -> Return v))
mterm2 = as_statte $
	 do
	 v <- get
	 put (not v)
	 return v
emterm2 = runst mterm2 False
-- (True,False)