[Haskell-cafe] rebinding >>= for restricted monads

[David Roundy]

Hello fellow haskellers,

I am wondering if anyone has an idea whether I'd run into trouble if I
rebound >>= in order to provide a more restricted monad.  My idea is to
define a class:

class WitnessMonad wm where
   (>>=) :: wm w w' a -> (a -> wm w' w'' b) -> wm w w'' b
   (>>)   :: wm w w' a -> wm w' w'' b -> wm w w'' b
   return :: a -> wm w w' a
   fail   :: String -> wm w w' a

which obviously just adds a couple of phantom types indicating the monad
state prior to and after each operation.  I actually rather like this
redefined monad, as it seems like it'd be useful in lots of places (e.g. a
restricted IO monad that disallows use of a file handle after it's
closed).

It seems to me like this would be a pretty cool kind of monad.  It'd allow
us to encode typechecked "properties" in a monad, and there'd be very
little restriction on how tricky those properties could be.  And we'd get
this all using the same do syntax we all love (and the new properties are
by definition sequential, so a monad is precisely what we want, only at the
type level).

One trouble I see is how to move an ordinary monad into the WitnessMonad
class.  Of course, they differ in kind, so we need to do something, but I'm
not sure what, and suspect that folks with experience using monad
transformers will immediately see the answer.  Of course, I want to be able
to use both my fancy witnessed monad and IO in the same module, and I want
to be able to use do notation for both of them.

I suppose we could easily define

data M m w w' c = M (m c)
lift = M
lower (M m) = m

instance WitnessMonad (M m) where
   f >>= g = lift $ Prelude.(>>=) (lower f) (lower . g)
   ...

but then we'd have to lift all our operations, so an ordinary IO function
in a module that used my fancy rebound do notation would look like

f :: IO Char
f = lower $ do lift $ putStr "Hello world"
               lift $ getChar

which seems rather heavy.  Can anyone think of syntax-light way to allow my
hypothesized rebound do-notation to also work with ordinary monads?
-- 
David Roundy
Department of Physics
Oregon State University