Heheh, this is straight off the qualifying exam I'm taking in 
a couple of weeks!  Have you read the excellent summary by 
Cardelli and Wegner?

  Luca Cardelli and Peter Wegner.  "On Understanding Types,
  Data Abstraction, and Polymorphism".  ACM Computing Surveys 1985.


My understanding is that universally quantified types
are just about the same as parameterized types.  Thus, a
C++ template is a universally quantified type, eg Stack is
universally quantified, while Stack<integer> is an instatiation
of that type and is *not* universally quantified.

To give a non-C++ example, consider the function identity:

	fun identity(x) = x

It's type is "Forall[a] a->a", that is, "for any type a, 
a function mapping an a to an a

Before you can use a univ. quantified item, you must instantiate
it like this:

	int_identity = identity[int]

Now int_identity is a version of the generic identity which only
accepts int's.  The type of int_identity is simply int->int.


Existential types I'm not so clear on myself, sorry.  Their *purpose*
is to define packages which can hide implementation details.  The
type of a package would be an existential type; you are only allowed
to take advantage of features of the package declared in the existential
type, even if the package has more features hidden inside.  

However, I'm not real clear on how the details work which implement
this purpose.....  Hopefully it will become clear by the time I take my
exam :)

Really, *most* of this type theory stuff is quite simple if you
know how to program.  But there's a significant overhead in learning
to wade through all the symbols!


Lex


PS -- I've been reading comp.lang.functional lately, and it sure
is nice not to have to worry about all these wierd kinds of types
when programming in Smalltalk.  In programming Smalltalk, types 
are usually more like "this is a dictionary-like thing"--things that,
for good and ill, computers and mathematicians cannot deal with :)



> 
> Perhaps you have read enough to help me understand uniquely,
> existentially and universally quantified types. That is one major
> aspect of type calculus that I am having trouble with, but which
> appears to show much potential for both genericity and efficiency.
> 
> -John
>