····@rnms1.paradyne.com (Alan Lovejoy) wrote:
>>> [the ideal programming language should] Be completely polymorphic.
>>I would like to see the definition of "polymorphic" (for my own education).
> You (and several other people, in email) asked for it! So here it is,
> along with three references:
> 1. "Polymorphic Programming Languages -- Design and Implementation" -- 1984
> David M. Harland, B.Sc., M.Sc., Ph.D., University Of Glasgow
> Halsted Press: a division of John Wiley & Sons
> Full polymorphism means that any component or aspect of a program, program
> component or programming language must behave as a value. Any and all
> values must be subject to inspection, modification, storage in memory,
> usage as a component part of some composite value, usage as a paremeter,
> usage as an operand in an expression, being computed as the result of
> evaluating an expression or function, and (re)definition of its form,
> structure, content or name. The protocol for invoking these common
> operations must be the same for all values, regardless of type.
> To say the same thing more concretely: numbers, characters, data types,
> procedures, variables, addresses, blocks, execution contexts, name bindings,
> scopes, processes and the number of bits in an integer must all be "first
> class objects."
You and Harland may mean that by "polymorphic", but the rest of the world
certainly doesn't. The mathematically understood senses of polymorphism are
(1) the Hindley type system, as implemented in Milner's ML and most functional
languages since, and (2) Girard's more powerful type system F, reinvented by
Reynolds and not fully implemented in any language I can think of (Fairbairn's
Ponder comes closest; Mitchell and Plotkin's SOL and Barendregt's TALE do it
on paper). There are umpteen mix-and-match combinations of these with other
ideas. It may be possible to construct a logical system combining the above
notion of dependent type with polymorphism; but nobody has ANY real idea how
to typecheck programs written in such calculi - a few flaky attempts to
implement some of Martin-Lof's type theories are the nearest anyone's got.
Nobody has the *faintest* idea how to coherently describe type systems in
which types are assignable values, as you ask for above. Putting all three of
these requirements (Milner or Girard polymorphism, dependent types, assignable
types) together in one formal calculus is presently quite unimaginable, still
less implementing the result in a type-safe programming language.
For another cautionary example, look at Cardelli's attempts to meet a few of
the same criteria in recent years: the result being a series of inconsistent
type systems attempting to provide a type of all types and an algorithm for
typechecking dependent types that nobody has any idea how to prove complete
(or refute, for that matter). Or look at Burstall and Lampson's Pebble
(dependent types and first-class bindings), still unimplemented ten years or
so after its design. This does not suggest we can expect any quick answers.
Yes, you might be able to hack together a language that provided all those
motherhood features (though as far as I know Harland's team at Linn haven't
managed to implement any significant fragment of Poly in the five years since
that book came out). But you wouldn't have a hope of reasoning about programs
written in it, and the appropriate formalism for verifying the compiler would
be chicken sacrifices and moving your mouse in pentagrams over the source code.
[ for references to this stuff, browse through a few recent LNCS's on data
types and the like ]
Despite this, the machine (REKURSIV/OBJEKT) that Harland designed to implement
these ideas seems to be a fast engine for running object-oriented code on.
--
Jack Campin * Computing Science Department, Glasgow University, 17 Lilybank
Gardens, Glasgow G12 8QQ, SCOTLAND. 041 339 8855 x6045 wk 041 556 1878 ho
INTERNET: ·····················@nss.cs.ucl.ac.uk USENET: ····@glasgow.uucp
JANET: ····@uk.ac.glasgow.cs PLINGnet: ...mcvax!ukc!cs.glasgow.ac.uk!jack