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

[ajb at spamcop.net]

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

Cheers,
Andrew Bromage