[Haskell-cafe] Re: Typed Lambda-Expressions withOUT GADTs

ajb at spamcop.net ajb at spamcop.net
Tue Jan 4 00:02:20 EST 2005

G'day all.

Quoting Conor McBride <ctm at cs.nott.ac.uk>:

> Where now? Well, counterexample fiends who want to provoke Oleg into
> inventing a new recipe had better write down a higher-order example.
> I just did, then deleted it. Discretion is the better part of valour.

Thankfully, I'm the sort of person who doesn't know when to stop.

Is this the sort of thing you had in mind?

-- 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

Andrew Bromage

More information about the Haskell-Cafe mailing list