wrapping parameterized types
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  rossberg@p... 
Subject:  Re: [Camllist] wrapping parameterized types 
"skaller" <skaller@users.sourceforge.net> wrote: > On Thu, 20070503 at 19:16 0400, Chris King 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. You have reason to be confused, because this is no existential type. Dirk Thierbach: >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) Actually, no, these are not equivalent. Only the following are: (\exists a. a) > b is equivalent to \forall a. (a > b) Here is the constructive proof. Assume: f : (exists a.a) > b g : forall a. (a > b) You can construct g from f and vice versa: g = \a. \a:x. f <a,x> f = \y:(exists a.a). let <a,x> = y in g a x Cheers,  Andreas