I disagree, to understand the differences one needs to define semantics for the terms first. To be concrete, what is an existential, a compile time existential, existential containers, existential values, existential types, existential box, opaqueness.
Then, differences between the meaning of these terms can be inferred and reoccurring discussions about them can be eliminated.
What does that mean?
Did you refer to the point of assigning an
any P to
some P types can be defined in terms of existential quantification, why aren't these existential types then?
Disagree, as this would imply
some P !=
some P at the type level, which is a contradiction.
I think you are talking about three entities here:
underlying type transparent to the type system:
underlying type opaque to the type system:
And yes, between the "underlying type transparent to the type system" and "the underlying type opaque to the type system" we have a many-to-one mapping, e.g.
Int can be mapped to type
Float can't be mapped to
(global1(),Int) as changing function
global1 to return Float would also change the transparent type to
The mapping from
some P to the "underlying type transparent to the type system" as well as to the "underlying type opaque to the type system" is one-to-many.
To see this, just change
return 2 to
return 2.0 in a function with
some Number as return type and the function is still sound.