Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cornell!uw-beaver!rice!flora!boehm
From: boehm@flora.rice.edu (Hans Boehm)
Newsgroups: comp.lang.c++
Subject: Re: Polymorphism
Message-ID: <3215@kalliope.rice.edu>
Date: 3 May 89 16:56:05 GMT
References: <5957@pdn.paradyne.com> <2841@crete.cs.glasgow.ac.uk> <3150@kalliope.rice.edu> <1898@etive.ed.ac.uk>
Sender: usenet@rice.edu
Reply-To: boehm@flora.rice.edu (Hans Boehm)
Organization: Rice University, Houston
Lines: 97

In article <1898@etive.ed.ac.uk> db@lfcs.ed.ac.uk (Dave Berry) writes:
>In article <3150@kalliope.rice.edu> boehm@flora.rice.edu (Hans Boehm) writes:
>>  There is some legitimate debate whether ML (without the recently added
>>  module system) should really be considered polymorphic.  ML-style
>>  polymorphism (like Ada generics) can always be replaced by macro expansion.
>>  (Unlike in Ada, this is not the usual implementation strategy.  Also unlike
>>  Ada, polymorphic expressions have a type that can be written down.)
>
>I'm having trouble understanding much of this debate.  In particular, how can
>ML style polymorphism be replaced by macro expansion?  Also, do you consider
>the module system to be polymorphic?  (I don't.  In fact it's much more like
>ADA than the core language.  It provides type parameterisation rather than
>polymorphism.)
>
>My definition of a polymorphic function is one that can be applied
>to objects of more than one type  ...

If we (at least temporarily) agree on this definition, there are still
at least two ways to accomplish this.  I'll use the identity function to
illustrate.

We may either continue to write the identity function as

    lambda x . x

and consider it to have type

    forall T . T -> T

Equivalently, we may introduce the type T as an explicit parameter to the
identity function.  We get

    lambda T . lambda x:T . x    or perhaps    lambda (T, x:T) . x

In Reynold's polymorphically typed lambda calculus the type of the
first form is written as something like

    Delta T . T -> T

In this case, the identity function must be invoked by applying it both
to a type and its "real" argument.

In their full generality (and ignoring questions related to the amount
of user specified type information) both views are equivalent.  There is
a direct correspondence between "forall" and "Delta".  Applications to
types correspond to replacement of a type variable by a specific type.
(See Leivant's paper in the 10th POPL proceedings for more details.)

ML (without modules) uses a restricted form of the first view, in which
"forall"s can appear only at the outer level of a type.  Types such as

    (forall T . T -> T) -> int

are illegal.  (Equivalently, there is no way to parametrize functions
with repect to polymorphic functions.)  At least theoretically, this is
a severe restriction.  If we take any applicative core ML program,
and substitute the right sides let declarations for left sides of let
declarations, we obtain an equivalent nonpolymorphic program.  For
example:

    let
	I = lambda x . x       ==>  ((lambda x: int -> int . x)
    in                                  (lambda x: int . x)) 3
	(I I) 3

In particular, the addition of an ML-style polymorphic let to the
simply typed lambda-calculus does not add to its expressive power.
The addition of fully general quantification or type parametrization
does, greatly.  How much this matters in practice is open to debate.
I would argue that it does matter, but probably primarily when it
comes to putting together large systems.

The standard ML module system uses a type parametrization view.
My impression is that it also limits parametrization to the outer level,
though perhaps not for a good reason.  (I could be completely wrong here,
though.)

What core-ML gains over the more general disciplines is that it appears
to be the most general system in which Hindley-Milner automatic type
inference is known to work completely, and thus the programmer has to specify
essentially no type information.  (Note that the type inferencer in fact
determines where type variables are instantiated.  Thus it could also
infer a program with explicit type parametrization and application, but
again all parametrization would have to be at the outer level.)

It loses in expressiveness.  Also the restrictions seem to necessitate
additional complications elsewhere (a separate module system, the treatment
of variables).  My (biased) opinion is that in the long run this isn't
worth it.  In the short run, it is probably the best system we know how to
implement really well.  But those of us working on more general systems
are gaining ...

In any case, I don't think that the ML type system should be used to DEFINE
the notion of polymorphism.

Hans-J. Boehm
boehm@rice.edu