foralls in class assertions

[Ashley Yakeley]

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