Re: [Caml-list] wrapping parameterized types

["Christopher L Conway" <cconway@cs.nyu.edu>]

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.uni-sb.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 forall-quantified 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 rank-2 polymorphism, and one can use rank-2 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 rank-2
> polymorphisms is very similar. Which is again a reason to make a
> connection between existential quantifiers and forall-quantifiers 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
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>