On Sun, Dec 17, 2006 at 11:12:27PM +0000, Ganesh Sittampalam wrote:
> 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
Yes, definitely, and the same with fail (although it's much less of an
issue with fail, for obvious reasons).
> >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.
Right, that would be another use of the class, but would require a highly
non-existential phantom type, and lots of use of classes. But people have
been working on stuff like that, only they have to always use "with"
functions to run in a new monad. I think it'd be much cleaner to be able
to use
do h <- openFile ...
c <- hGetChar h
...
closeHandle h
c' <- hGetChar h
and have a type error on the last line, because the handle's already been
closed. No nested monads required, if you can use a WitnessMonad.
> >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.
Right. The big issue (which I've asked about on haskell-cafe) is whether
we could mix ordinary Monads with WitnessMonads in the same module
somehow...
--
David Roundy
http://www.darcs.net
_______________________________________________
darcs-devel mailing list
[email protected]
http://www.abridgegame.org/cgi-bin/mailman/listinfo/darcs-devel
