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:  Dirk Thierbach <dthierbach@g...> 
Subject:  Re: [Camllist] wrapping parameterized types 
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