wrapping parameterized types

Christopher L Conway

Chris King

skaller
 Dirk Thierbach

rossberg@p...

Andrej Bauer

Dirk Thierbach
 Christopher L Conway

Dirk Thierbach

Andrej Bauer
 Christopher L Conway

skaller

Chris King
[
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:  Christopher L Conway <cconway@c...> 
Subject:  Re: [Camllist] wrapping parameterized types 
Can anyone point me to where the semantics of these, um, existential type declarations are defined? This topic is mentioned only scantly in the manual. I'd also be interested in pointers to the underlying type theory. Thanks, Chris On 5/4/07, Dirk Thierbach <dthierbach@gmx.de> wrote: > Andrej Bauer wrote: > >rossberg@ps.unisb.de wrote: > > >> 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. > > Well, as classical logical formulae, they clearly are :) Which IMHO > is enough to explain the name. Notice I said "pretend", and didn't use > the word "intuitionistically". > > >> Only the following are: > >> > >> (\exists a. a) > b is equivalent to \forall a. (a > b) > > But that doesn't explain why the usage in the example is called > "existential". All "normal" types are forallquantified on the outside, > so this isn't really a new feature in any way. > > > Right, and this is in accordance with the terminology. > > Well, then maybe I don't understand the terminology :) > > > Note that Dirk misread the precedence of operators: > > No, I didn't, but maybe I was to terse. The point is that records > in OCaml allow rank2 polymorphism, and one can use rank2 polymorphism > to encode existential types. The crucial point in the example is here: > > >>>> type 'b mylistfun = { listfun: 'a. 'a list > 'b } > [...] > >>>> val app_to_mylist : 'a mylistfun > mylist > 'a = <fun> > > So, ignoring records, app_to_mylist has the type > > app_to_mylist : (\forall 'a. 'a list > 'b) > mylist > 'b > > Now, "morally" this is similar to > > app_to_mylist : \exists 'a. ('a list > 'b) > mylist > 'b > > as pointed out before. So one can indeed pretend that 'a is > existentially qualified in this function. And this is important, > because that's what makes the whole thing work ("there is a type 'a > such that app_to_mylist executes, but we don't now in advance which > one"). And the encoding of "real" existential types using rank2 > polymorphisms is very similar. Which is again a reason to make a > connection between existential quantifiers and forallquantifiers in > negative positions, and call such an encoding "existential type". > > OTOH, the conversion from (\forall 'a. 'a list > 'b) to > ((\exists 'a. 'a list) > b) really doesn't explain anything. Or maybe > it does, and I don't understand it, but so far, the other explanation > makes a lot more sense to me. > >  Dirk > > _______________________________________________ > Camllist mailing list. Subscription management: > http://yquem.inria.fr/cgibin/mailman/listinfo/camllist > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/camlbugs > >