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'
Hello, Apologies if I missed the point of the post (I couldn't fnid the original), but there is yet another even simpler way to define such term algebras, and it works in Haskell'98. The idea is that operations are paremeterized by their continuation, i.e. "bind" is spread across the computations:
data State s a = Return a | Set s (State s a) | Get (s -> State s a)
instance Monad (State s) where return x = Return x
Return x >>= k = k x Set s m >>= k = Set s (m >>= k) Get f >>= k = Get (\s -> f s >>= k)
get = Get Return set s = Set s (Return ())
In general, a primitive of type: p :: a -> M b becomes a constructor of type: data M c = Return c | ... | P a (b -> M c) and then the operation becomes: p :: a -> M b p a = P a Return The laws defining how the operations of the monad work are then captured in the monadic intepreter:
run :: State s a -> s -> (a,s) run (Return a) s = (a,s) run (Set s1 k) s = run k s1 run (Get f) s = run (f s) s
This seems a lot simpler which is why I though I'd post it.
-Iavor
On Tue, 4 Jan 2005 00:08:04 -0800 (PST), oleg@pobox.com
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' _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
G'day all.
Quoting Iavor Diatchki
Apologies if I missed the point of the post (I couldn't fnid the original), but there is yet another even simpler way to define such term algebras, and it works in Haskell'98.
The idea is that operations are paremeterized by their continuation, i.e. "bind" is spread across the computations:
Ralf Hinze advocated this approach (based on a technique by John Hughes) in his paper "Deriving Backtracking Monad Transformers". As you can see from the backtracking with pruning ("cut") monad that he derives, though, it's not necessarily a "simple" derivation, and there is a creative step required, in working out what the context (in the case of State, the continuation) actually is. However, the point of the exercise was not to find a way to express a state monad. The point was to find a way to express it easily, as an attempt to find the right interface before going to the trouble of deriving an efficient implementation which is optimised for that interface. The GADT solution is one way to do this, and IMO it's pretty close to the easiest. BTW, if someone would like an "interesting" monad to play with, here is one that I've been playing with for a while. It's a nondeterminism monad transformer with negation-as-failure and if-then-else with soft cut. The appropriate contexts/continuations for an efficient implementation (using the Hughes/Hinze technique) turn out to be quite difficult to find. The operations that we need to implement are: - the Monad operations (return and bind), - the MonadTrans operation (lift), - the MonadPlus ones (mzero and mplus), and - one other operation, which plays the role of logical if-then-else. Logical if-then-else has this signature: mif :: LogicT m a -> (a -> LogicT m b) -> LogicT m b -> LogicT m b Intuitively, this takes three arguments: the "condition", the "then" case and the "else" case. This obeys the "obvious" laws of if-then-else: mif (return a) t e = t a mif (mzero) t e = e mif (mif c t' e') t e = mif c (\x -> mif (t' x) t e) (mif e' t e) plus the "soft cut" law: mif (return a `mplus` m) t e = t a `mplus` (m >>= t) The soft cut law is the one that stuffs up the more obvious candidates for the passed context, because of this non-identity: mif (c1 `mplus` c2) t e /= mif c1 t e `mplus` mif c2 t e Cheers, Andrew Bromage
In article <20050105201737.s24g48oo0w8w4occ@webmail.spamcop.net>, ajb@spamcop.net wrote:
Logical if-then-else has this signature:
mif :: LogicT m a -> (a -> LogicT m b) -> LogicT m b -> LogicT m b
Intuitively, this takes three arguments: the "condition", the "then" case and the "else" case. This obeys the "obvious" laws of if-then-else:
mif (return a) t e = t a mif (mzero) t e = e mif (mif c t' e') t e = mif c (\x -> mif (t' x) t e) (mif e' t e)
plus the "soft cut" law:
mif (return a `mplus` m) t e = t a `mplus` (m >>= t)
The soft cut law is the one that stuffs up the more obvious candidates for the passed context, because of this non-identity:
mif (c1 `mplus` c2) t e /= mif c1 t e `mplus` mif c2 t e
Is mif reducible to some "melse" with mif c t e = do ma <- (c >>= return . Just) `melse` (return Nothing) case ma of Just a -> t a Nothing -> e ...? -- Ashley Yakeley, Seattle WA
participants (4)
-
ajb＠spamcop.net -
Ashley Yakeley -
Iavor Diatchki -
oleg＠pobox.com