Proposal: ExplicitForall

[Niklas Broberg]

Hi all,

(I'm writing this to several lists since it involves GHC
(implementation of extensions), cabal (registration of extensions) and
some future Haskell standard (formalisation of extensions).)

In my quest to implement all known syntactic extensions to Haskell in
my haskell-src-exts package, I've become painfully aware of the
sometimes ad-hoc nature that these extensions have been added to GHC.
This should not be taken as criticism per se, GHC is awesome and I'm
sure a lot of thought and research has gone into all of these
extensions. I think the problem (from my point of view) is rather that
most of the extensions are only really "interesting" on a type system
level, whereas the syntactic level is rather trivial, and thus the
latter has (rightly) gotten far less formal attention. I hope my
putting the light on these issues will be a help and a kickoff towards
improving the state of formalisation of the known and registered (with
Cabal) extensions.

One of the most blatant and (to me) problematic such issues is the
matter of using 'forall'. GHC has a number of extensions relating to
the use of forall-quantified types in various interesting ways. With
none of these extensions on, forall is not considered a keyword, so
the syntax with explicit forall quantification cannot be used at all
('forall' is considered a varid). However, with *any* extension on
that relates to forall-quantified types, forall is a keyword, and can
syntactically be used in types *anywhere*. This doesn't mean all such
types will pass the type checker, most of them won't in fact, but
syntactically there is really no (or at least very little) difference.

Conceptually, all of these extensions (specifically
PolymorphicComponents, Rank2Types, RankNTypes, LiberalTypeSynonyms and
ScopedTypeVariables (and strangely also ExistentialQuantification))
thus have one thing in common. They all enable syntactically
forall-quantified types. They allow different uses of these types as
far as the type system is concerned, but syntactically there is no
difference between type and type (in fact there cannot be, as I
discussed in a recent blog post [1]).

Funnily enough there are also some uses of forall-quantified types
that are common to all of these extensions - using a forall just to
make polymorphism explicit in a type doesn't change anything as far as
the type system is concerned, so e.g. the types '(Eq a) => a -> Bool'
and 'forall a . (Eq a) => a -> Bool' are equivalent. The latter type
can be given to a function when any of the listed six extensions are
given, even if most of them have nothing to do with this at all!

So, what I'm getting at is an idea that Isaac Dupree gave as a comment
to my blog post. He said:

   "I wish there was a plain old ExplicitForall extension that enabled
the keyword in types (without extending the type checker -- only like
(id :: forall a. a -> a) would be allowed)".

I think this is a really great idea. I find it conceptually appealing,
since I think it covers exactly that blind spot that is the seemingly
unintended intersection between all these extensions. And it also
makes the separation of concern between the syntactic level and the
type system more clear. Any formalisation of any of the type system
extensions would not need to bother with syntactic details, but can
simply be said to imply ExplicitForall.

I would thus like to propose the following formalisation of the
ExplicitForall extension:

=========================================
ExplicitForall enables the use of the keyword 'forall' to make a type
explicitly polymorphic. Syntactically, it would mean the following
change to Haskell 98:

* 'forall' becomes a reserved word.
* '.' (dot) becomes a special (not reserved) operator.
* The following syntactic rule changes:

type      -> 'forall' tyvars '.' type
           | context '=>' type
           | ftype

ftype     -> btype '->' type
           | btype

gendecl   -> vars '::' type

It does not allow the use of explicitly polymorphic types in any way
not already allowed by Haskell 98 for implicitly polymorphic types.
=========================================

One thing to note is that I haven't touched the matter of
ExistentialQuantification in the above. Syntactically this is a
different beast entirely, and could well be handled separately, though
it's really an artifact of the way we (by default) write our data type
declarations. Using GADT-style declarations, existential
quantification goes nicely along with the others by following the same
syntactic rules for types, even though from a type system it is of
course still quite different from the rest. But with the ordinary
Haskell 98 declaration style, we could define the syntactic part of
the ExistentialQuantification extension as the following:

=========================================
ExistentialQuantification allows data constructors to take
existentially quantified arguments. Syntactically, it means the
following changes to Haskell98:

* 'forall' becomes a reserved word.
* '.' (dot) becomes a special (not reserved) operator.
* The following syntactic rule changes:

constrs   -> econstr_1 '|' ... '|' econstr_n

econstr   -> ['forall' tyvars '.' [context '=>']] constr

=========================================

My hope is that you'll all agree with me on the need and rationale for
the ExplicitForall extension, and that my proposal for formalisation
is good enough for adoption. I feel much less strongly about
ExistentialQuantification, and would love to hear some more input on
that matter, but I do think it needs to be addressed one way or the
other.

Thoughts?

Cheers,

/Niklas


[1] http://nibrofun.blogspot.com/2009/06/whats-in-forall.html