At 2002-07-22 04:58, Simon Peyton-Jones wrote:

This business of having 'foralls' in a context (whether for a class or a function) is not hard to implement in principle, but in practice it'd take few days of hacking I guess. And, more to the point, thinking. What are the interactions with functional dependencies or implicit parameters? (Maybe none, but I've been caught before.)

So it's really waiting for someone to say "having foralls in contexts would change my life and I would love you for ever", rather than "it'd be nice".

Simon "lazy evaluation" PJ

OK, I can't say it would change my life but I did come up with a rather more motivating example. I guess the best I can offer is "I'll buy you a drink next time I'm back in Cambridge" (I have family there, so it does happen). I want to implement typed exceptions somewhat similar to Java. Code would declare type using an "ExceptionMonad" of kind (* -> * -> *): class (forall ex. Monad (mm ex)) => ExceptionMonad mm where { throwX :: x -> mm x a catchX :: mm xa a -> (xa -> mm xb a) -> mm xb a; } Notice how the types of throwX and catchX precisely mirror those of return and (>>=). Now I could write code that throws different kinds of exceptions like this: data FooException = MkFooException String; foo :: (ExceptionMonad mm) => Char -> mm FooException Integer; foo c = ... data BarException = MkBarException | FooBarException FooException; bar :: (ExceptionMonad mm) => mm BarException Integer; bar = do { a <- catchX (foo 'q') (\fx -> throwX (FooBarException fx)); return (a + 1); } This allows you to have typed structured exceptions more easily, which I think is preferable in many cases to relying on "fail" with its String argument... -- Ashley Yakeley, Seattle WA