help from the community?

[Iavor Diatchki]

Hello,

On 1/26/07, Malcolm Wallace <Malcolm.Wallace at cs.york.ac.uk> wrote:
> > [ scheme  = 'forall' tvars '.' opt_ctxt type ]
> > The non-terminal 'tvars' is a sequence of type variables that are
> > separated by blank spaces. We have a choice if we should allow empty
> > quantifier sequences.
> > PROPOSAL: be liberal:
> >   * allow empty quantifier lists
> >   * allow variables that are not mentioned in the body of a type (but warn)
> >   * allow predicates that do not mention quantified variables (but warn?)
>
> I cannot see how an empty list of tyvars is useful or desirable in
> practice:
>     data Foo = Foo (forall . Int)
> is equivalent to just
>     data Foo = Foo Int
> so why bother to permit the former?  It probably indicates some error in
> the thinking of the programmer, so the compiler should bring it to her
> attention.
>
> On the other hand, I can imagine a use for phantom type variables in the
> quantifier (especially if they occur in multi-parameter predicates, but
> not in the type).  So I think accepting them with a warning is
> reasonable.
>
> I can also imagine predicates that do not mention locally-quantified
> variables - the assumption must be that they mention variables bound on
> the LHS of the datatype decl instead?  e.g. the Show predicate here:
>
>     data Foo a b = Foo a b
>                  | Bar (forall c . (Show b, Relation b c) => (b,c))
>
> Hmm, maybe a simpler version of this example would illustrate what you
> mean by the proposal (first of the three bullets) to allow an empty
> quantifier list:
>
>     data Foo a b = Foo a b
>                  | Bar (forall . Show b => b)
>
> In which case, does this even count as a polymorphic component at all?
> Is it not rather GADT-like instead?
>
>     data Foo a b where
>       Foo :: a -> b -> Foo a b
>       Bar :: Show b => b -> Foo a b

I was thinking that we should allow those special cases because I
could not see a reason to disallow them (rather then having a
compelling example to use them).   You make a good point though, that
some of them might indicate an error in the program.  So, I guess, the
main decision is: do we want to make them illegal (i.e., require an
error) or suggest that implementations report a warning?  I have no
strong feelings either way, but I guess we need to pick something.

> > Constructor that have polymorphic components cannot appear in the
> > program without values for their polymorphic fields.
>
> I didn't fully understand this requirement.  If Haskell-prime gets
> rank-2 or rank-n types, then do we need to restrict constructors in this
> way?

The issue is the same as for rank-2 types.  My suggestion is based on
the design adopted by Hugs.  The basic idea is that by requiring that
functions with rank-2 types (in particular, constructors that have
polymorphic fields) are applied to all their polymorphic arguments, we
ensure that expressions can be typed by simple types as in HM (and not
type schemes).

On the pragmatic side this has the benefit that the rank-2 type
extension is quite easy to add to a Haskell'98 implementation:  the
arguments to rank-2 functions are checked pretty much in the same way
as expressions with explicit type signatures.  The only difference is
that the type signature may contain free type variables which doesn't
happen in Haskell 98.

On the theoretical side we have the benefit that this fairly
conservative extension to the type system (we are still working
essentially in HM) gives us a big increase in expressiveness (e.g., we
can encode System F programs in Haskell).  The reason that the type
system extension is quite simple is that Haskell 98 compares types for
equality by name (as opposed to examining their structure).

Other alternatives are systems like MLF (by Didier Le Botlan and
Didier Rémy) and the relaxed system implemented by GHC.  I think that
they are both quite interesting but I must admit that for the purposes
of Haskell' I am partial to the simplicity of Hug's design.  The
reason is that I feel that I can explain it to an ordinary Haskell
programmer without too much difficulty and it has been sufficient for
the situations when I've used rank-2 types.  I could be unfairly
biased, however, which is why discussions are most welcome! :-)

-Iavor