| GHC is a little bit more permissive than Hugs here;
| but not as much as you would like.
I'm not sure that's correct. As Ralf had noticed, Hugs allows explicit
foralls on type declarations. This is an undocumented extension that I
implemented during a recent train journey across the French countryside,
having just learnt that you supported this syntax in GHC. (The joys of
mobile computing!) I believe/hope that Hugs is now just as permissive as
GHC in its treatment of this feature; after all, my motivation in adding
it was to reduce unnecessary differences, and this was an easy change for
me to make.
| 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; ...
Indeed you could, and this is something that I've argued for in the past.
It's a mistake to say that these two types are isomorphic but different.
That may be true in the GHC implementation, but it doesn't mean that we
have to adopt the same interpretation at the Haskell source level. After
all, the GHC/System F interpretation of a polymorphic definition like:
let id = \x -> x
in ...
treats id as a function of two parameters; an implicit type parameter and
the explicit x parameter. But you don't attempt to enforce a monomorphism
restriction for this definition, nor do you expect any loss of sharing.
This is one example of a place where the semantics of Haskell differs from
what the GHC approach suggests ... but no problems occur because we know
how to map smoothly between the two.
In some models, the two types above have exactly the same meaning; perhaps
this is the interpretation that we would like to have in Haskell. (Apart
from anything else, it's also more consistent with the treatment of let.)
In this case, a -> forall b.t can be treated simply as surface syntax for
forall b. a -> t. There's no need for any additional special treatment,
and it doesn't clash with any other syntax that we're already using.
So now you want to know why it's useful. For one thing, it's important
because it allows a programmer to express themselves more accurately in
the types that they write. For example, if I want to explain how the
constructors of the Boolean or list types can be mapped into corresponding
folds, then I really do want to be able to write types like:
cond :: Bool -> (forall a. a -> a -> a)
fold :: [a] -> (forall b. b -> (a -> b -> b) -> b)
It can also make types more readable. For example, if you see a type:
forall a. t1 -> t2 -> t3 -> .... -> t
then you have to read the arguments t1, t2, t3, ... to see if they make
use of a. If you write:
t1 -> t2 -> t3 -> .... -> (forall a. t)
then the scoping of a is much clearer and easier to understand. Finally,
it can be particularly useful if we make a further extension to allow foralls
to appear in type synonyms. For example:
type Church = forall a. (a -> a) -> (a -> a)
succChurch :: Church -> Church
succChurch n = \f x -> n f (f x)
(This example uses church numerals and may seem somewhat obscure, but several
people have told me that they'd like to be able to do similar things in other
settings.) If you won't allow the forall on the left of the -> then you will
force me either to write something like:
type Church a = (a -> a) -> (a -> a)
succChurch :: (forall a. Church a) -> Church a
...
This is a pain because (1) it doesn't expose the real symmetry here--that
succChurch is essentially a function mapping values of a particular type to
values of the very same type, and (2) the "forall" really belongs to the
definition of Church numerals, and isn't something that I want to repeat
every time I use one.
Or perhaps you would have me write:
newtype Church = MkChurch (forall a. (a -> a) -> (a -> a))
...
succChurch (MkChurch n) = MkChurch (\f x -> n f (f x))
This is a pain because it means that I have to clutter the definition of my
values with nasty newtype constructors and coercions, just so that I can write
the types in a clear form.
I'm not suggesting---at this stage---that something like this should be in
Haskell. But I think there's a very strong argument for experimenting with
this feature in our existing implementations.
All the best,
Mark
----------------------------------------------------------------------------
[EMAIL PROTECTED] Pacific Software Research Center, Oregon Graduate Institute
Looking for a PhD or PostDoc? Interested in joining PacSoft? Let us know!
