foralls in class assertions

[Ashley Yakeley]

At 2002-02-19 09:21, Simon Peyton-Jones wrote:

>I don't know if it makes sense.   You've written down some syntax,
>but it's not clear to me what you intend by it.

Hmm... it should be straightforward...

>	instance (forall a. Eq a => Eq (f a)) => Eq (Rose f a) where..

I assume that the 'a' quantified in (forall a. ...) is not the same as 
the 'a' in 'Rose f a'?

>|     instance
>|         (
>|         forall a. HasIdentity (m a a),
>|         forall a b c. Composable (m b c) (m a b) (m a c)
>|         ) =>
>|      Category m;

This means 'if for all a, "HasIdentity (m a a)", and also for all a b c, 
"Composable (m b c) (m a b) (m a c)", then "Category m"'.

"(forall a. HasIdentity (m a a))" as a class assertion declares a 
property of m. It says that for all types a, there's an instance 
"HasIdentity (m a a)".

>| Or even allow the foralls their own context:
>| 
>|     foo :: (forall a. (C a b) => D a c) => T b c;

This means foo has type (T b c), where for every type a for which there's 
an instance "C a b", there's an instance "D a c".

>|     class
>|         (
>|         forall a. HasIdentity (m a a),
>|         forall a b c. Composable (m b c) (m a b) (m a c)
>|         ) =>
>|      Category m;

Personally I think the 'superclass' arrow in class declarations should 
point the other way, as in '<='. After all, instances of the class imply 
instances of the superclasses, not the other way around.

But that aside, this means '"Category" is a class on m, provided that for 
all types a, there's an instance "HasIdentity (m a a)", and also for all 
types a b c, there's an instance "Composable (m b c) (m a b) (m a c)"'.


-- 
Ashley Yakeley, Seattle WA