Initial (term) algebra for a state monad

Andrew Bromage wrote:

<<
-- WARNING: This code is untested under GHC HEAD

data State s a
  = Bind :: State s a -> (a -> State s b) -> State s b
  | Return :: a -> State s a
  | Get :: State s s
  | Put :: s -> State s ()

instance Monad (State s) where
    (>>=) = Bind
    return = Return

instance MonadState s (State s) where
    get = Get
    put = Put

runState :: State s a -> s -> (s,a)
runState (Return a) s = (s,a)
runState Get s = (s,s)
runState (Put s) _ = (s,())
runState (Bind (Return a) k) s = runState (k a) s
runState (Bind Get k) s = runState (k s) s
runState (Bind (Puts) k) _ = runState (k ()) s
runState (Bind (Bind m k1) k2) s = runState m (\x -> Bind (k1 x) k2) s
>>

The following is the code that does run, on GHC 6.2.1. Typeclasses are
just as good at pattern-matching as (G)ADT, and GHC is quite good at
suggesting the constraints that I have missed. The latter comes quite
handy when one programs half-asleep.


{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

module B where

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

-- data State s a
--   = Bind :: State s a -> (a -> State s b) -> State s b
--   | Return :: a -> State s a
--   | Get :: State s s
--   | Put :: s -> State s ()

class RunBind t s a => RunState t s a | t s -> a where
    runst :: t -> s -> (s,a)

data Bind t1 t2 = Bind t1 t2
data Return t = Return t
data Get = Get 
data Put t = Put t


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

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

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



test1 (a::a) = runst (do
                 x <- (return a :: Statte Char a)
                 y <- get
                 put 'b'
                 return (y,x)) 'a'
test1' = test1 "ok"

test2 = runst (return True :: Statte Char Bool) 'a'