Ralf,
GHC is a little bit more permissive than Hugs here;
but not as much as you would like. I'm a bit reluctant
to encourage
f :: Int -> (forall a. a->a)
because this really is a different type in GHC to
f :: forall a. Int -> a -> a
They are isomorphic, but take their type arguments in a different order.
Maybe I could treat those two Haskell-language-level type signatures as
notation for the second of the two; but it looks a like a tiresome
little swamp that I'm not keen to jump into unless it is really
ruining your life.
Simon
| -----Original Message-----
| From: Ralf Hinze [mailto:[EMAIL PROTECTED]]
| Sent: 05 November 1999 13:53
| To: [EMAIL PROTECTED]
| Subject: forall
|
|
| This is not a bug report but a suggestion concerning a Hugs -98
| feature: universal quantifiers. BTW I refer to the September 1999
| Version.
|
| First of all, I just discovered that you can now make universal
| quantification explicit. That's great!
|
| > data List a = Nil | Cons a (List a)
|
| > mapList :: forall a a'.(a -> a') ->
| (List a -> List a')
| > mapList mapa Nil = Nil
| > mapList mapa (Cons v vs) = Cons (mapa v) (mapList mapa vs)
|
| However, slight variations cause syntax errors.
|
| > mapList :: (forall a a'.(a -> a') ->
| (List a -> List a'))
| > mapList :: forall a.forall a'.(a -> a')
| -> (List a -> List a')
|
| ERROR: Syntax error in type signature (unexpected keyword "forall")
| ERROR: Syntax error in type signature (unexpected `;',
| possibly due to bad layout)
|
| Furthermore, universal quantifiers can only appear on the top level
| (ignoring rank-2 type sigantures for the moment). It is not
| possible to
| write `t -> forall a.u' even though the type is equivalent to `forall
| a.t -> u' provided `a' does not appear free in `t'. So I must write
|
| > data Twice f a = Twice (f (f a))
|
| > mapTwice :: forall f f' a a'.(forall b
| b'.(b -> b') -> (f b -> f' b'))
| > -> (a ->
| a') -> (Twice f a -> Twice f' a')
| > mapTwice mapf mapa (Twice v) = Twice (mapf (mapf mapa) v)
|
| instead of
|
| > mapTwice :: forall f f'.(forall b b'.(b
| -> b') -> (f b -> f' b'))
| > -> (forall a
| a'.(a -> a') -> (Twice f a -> Twice f' a'))
|
| which is more logical (for what I have in mind).
|
| I think that these problems can be solved if the type language
| is extended by a production for quantified types `forall
| <tvars>.<type>'.
| Then in a second pass it is checked whether the type signature has a
| rank less or equal two. This extension would also permit
| quantified types
| in type signatures.
|
| What do you think?
|
| Ralf
|
