On Sun, 17 Dec 2006, David Roundy wrote:
I was just this morning wondering how best to implement the pending
handling with GADTs. It's actually tempting to rebind (>>=) and use a
modified monadic notation, which would actually be a monad with type
guarantees.
I'm thinking something like:
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
I think the type of return is wrong, it needs to be:
return :: a -> wm w w a
Otherwise (x >>= return) :: wm w w'' b when x :: wm w w' b, which violates
the monad laws at the type level and makes the witnesses useless.
Specific instances of WitnessMonad would provide values where w /= w'.
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).
I don't think you could do that without encoding lots of stuff in the
phantom type.
The trouble is that all the core patch code would need to be rewritten.
And we'd need to use -fno-implicit-prelude and hide the "standard" Monad.
We also wouldn't be able to mix use of the two in the same module.
Hopefully it'd be mostly a case of changing the type signatures, rather
than actually rewriting code, though.
Cheers,
Ganesh
_______________________________________________
darcs-devel mailing list
[email protected]
http://www.abridgegame.org/cgi-bin/mailman/listinfo/darcs-devel
