Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!csd4.milw.wisc.edu!lll-winken!uunet!pdn!rnms1!alan
From: alan@rnms1.paradyne.com (Alan Lovejoy)
Newsgroups: comp.lang.c++
Subject: Re: Polymorphism
Message-ID: <5972@pdn.paradyne.com>
Date: 23 Apr 89 06:32:44 GMT
References: <5957@pdn.paradyne.com< <2841@crete.cs.glasgow.ac.uk>
Sender: news@pdn.paradyne.com
Reply-To: alan@rnms1.paradyne.com (Alan Lovejoy)
Organization: AT&T Paradyne, Largo, Florida
Lines: 47

In article <2841@crete.cs.glasgow.ac.uk< jack@cs.glasgow.ac.uk (Jack Campin) writes:
<> I wrote:
<> 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.

I deliberately defined it as extremely as I could.  I knew it was
controversial. I wanted to start a discussion.  It worked, didn't it?

<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).  

<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.

The definition I gave is motivated by denotational semantics.  Whether its
mathematical properties are completely understood is a completely separate
question. All I gave was a definition.  I didn't say that any language
does or could live up to it, or that it would be worthwile to create a
language that could.


Alan Lovejoy; alan@pdn; 813-530-2211; AT&T Paradyne: 8550 Ulmerton, Largo, FL.
Disclaimer: I do not speak for AT&T Paradyne.  They do not speak for me. 
_________________________Design Flaws Travel In Herds_________________________
Motto: If nanomachines will be able to reconstruct you, YOU AREN'T DEAD YET.