Re: ExistentialQuantifier

Ross Paterson wrote:

I don't think the original name is inappropriate: the feature described is certainly existential quantification, albeit restricted to alternatives of data definitions.

I think that "existential quantification" should mean, well, existential quantification, in the sense that term is used in logic. I don't like the idea of using it for the feature currently implemented with "forall" in front of the data constructor, given that these type variables are universally quantified in the data constructor's type. How about changing the name to "existential product types" or "existential tuples"? I would even suggest "boxed types", but that's already taken. -- Ben