Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!husc6!rice!flora!boehm
From: boehm@flora.rice.edu (Hans Boehm)
Newsgroups: comp.lang.c++
Subject: Re: Polymorphism
Message-ID: <3150@kalliope.rice.edu>
Date: 22 Apr 89 22:57:57 GMT
References: <5957@pdn.paradyne.com> <2841@crete.cs.glasgow.ac.uk>
Sender: usenet@rice.edu
Reply-To: boehm@flora.rice.edu (Hans Boehm)
Organization: Rice University, Houston
Lines: 58


  I would like to take issue with a frew of the points raised in the recent
discussion of polymorphism, especially by Jack Campin's article.

1. ML is traditionally viewed as the canonical example of a polymorphically
  typed programming language.  Nonetheless there is some legitimate debate
  whether the language (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.) This is not true of
  the Girard-Reynolds system.
2. Several programming languages based in the Girard-Reynolds lambda
  calculus have been successfully implemented and used.  The ones I know
  about are Russell (with which I have been involved), the language
  underlying IBM's Scratchpad II symbolic algebra system, and Dave Mathews'
  Poly.  Some recent language designs from Waterloo probably also fit into
  this category.  The type systems used by these languages are all variations
  on the Reynolds system.  But they all must address essentially the same
  issues that would have arisen if the Reynolds system had been used directly.
3. It is no harder to define the semantics of one of these languages than
  that of any other real programming languages.  This is an issue that is
  largely independent of the type system.  Indeed, the semantics are usually
  specified without reference to the type annotations in the program.
  Empirically, a program written in one of these languages is much more
  likely to be correct (once it compiles) than a C or Lisp program.  (The
  same observation applies to ML, for those programs that can easily be
  written in ML.  Unfortunately, these statements are all based on anecdotal
  evidence.)
   Note that giving a semantics to a program is orthogonal to that of giving
  semantics to types, since we usually specify program semantics as though
  the program were untyped.  Giving semantics to types, and proving that the
  type system insures certain execution time properties is harder, and is
  certainly still a subject of research.  But the real problem here is that
  we don't entirely understand what properties should be insured by a type
  checking system, independent of the particular language.  I claim that this
  problem is as hard to solve for Pascal as it is for Russell or Scratchpad II.
4. Type checking (with programmer specified types) is well understood for
  these languages.  Type RECONSTRUCTION (or inference) in the ML sense
  is harder, but is also beginning to be understood.  See the paper by
  Frank Pfenning in the last Lisp conference, or one of the two papers on
  the subject in the upcoming SIGPLAN conference.  To date, this has probably
  been the most serious implementation obstacle for these languages.
5. A number of these systems allow a type of all types, which is an "element
  of" itself.  This causes problems with the "propositions as types" analogy,
  which is important in other contexts.  It also causes some slight
  complications in the implementation, since there is no longer a clear
  distinction between type and non-type values.  Thus types may have to be
  represented at run-time.  (However it usually doesn't matter what they
  are represented as, only that space is reserved for them as for other
  values.  Even this can usually be optimized away.)
  I know of no real sense in which it makes a programming language
  type system inconsistent.  (The "proposition as types" analogy is also hard
  to preserve if it is possible to write any programs that do not terminate.
  I know of no real programming languages in which all programs terminate.)

Hans-J. Boehm
boehm@rice.edu