Re: [Caml-list] wrapping parameterized types

[Dirk Thierbach <dthierbach@gmx.de>]

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