On Fri, May 04, 2007 at 11:10:03AM +1000, skaller wrote:
> On Thu, 2007-05-03 at 19:16 -0400, Chris King wrote:
> > On 5/3/07, Christopher L Conway <cconway@cs.nyu.edu> wrote:

> > The solution is to use existential types.  In a record, you can tell
> > O'Caml that a particular function _must_ be polymorphic:
> > 
> > type 'b mylistfun = { listfun: 'a. 'a list -> 'b }

> I'm still confused why this is called an existential, when
> clearly the quantification is universal.

It's because the universal quantifier is in a "negative" position,
which is equivalent to an existential quantifier on the outside.
Just pretend they are logic formulae instead of types, and then

(\forall a. a) -> b   is equivalent to   \exists a. (a -> b)

using DeMorgan's rule.

- Dirk