Speaker: Teng Zhang
Chapter: Existential types
SCW office hours, Wed 9AM
Reminder: class starts at 1:30.
Just yesterday, I watched Yaron Minsky's CUFP 2016 talk from Japan and it turns out to have a short discussion of existential types in OCaml. See around 22 min point for this discussion (though you should watch the whole thing).
Note from Kenny: I gave a lecture at Hendrix last year building on functional queues, and making even fancier queues using Okasaki's lazy scheduling data structures. Some of that is here.
-
The naming seems to suggest so, we even have an encoding from universal to existential, but I don't really see how existential types relate to our intuition of existential quantification in logic?
[SCW: In constructive logic, the proof of an existential proposition is a pair of a witness and a proof that the witness satisfies the property. We can think of existentials as a pair of a type (witness) and a term that uses that type to create the abstract module.]
-
In the presentation of abstract data types, I can see how this relates to interfaces/implementation in languages like c++/java. But why is it presented as an existential type? I don't really see the connection between existential quantification and interfaces.
In Haskell, we could use typeclasses as constraints when declaring a function that's reminiscent of the interface/implementation/client interaction presented in this chapter. For example,
myShow :: (Show a) => a -> String myShow = showCan "Show a" here be considered as an existential type? Where does existential quantification come into the picture in this case?
[SCW: "Show a" is like tau part in "exists t. tau". It is the description of a structure with an abstract type component (i.e. a). We don't actually create the existential value much in Haskell but we could. It would be a value of type
data ExShow where Pack :: Show a => ExShow --- watch for ambiguity hereThen we can open this package when we pattern match on a value of this type. However, that's a bit silly, so in Haskell we often use the isomorphism between the types:
f :: (exists a. tau) -> tand g :: forall a. tau -> t when a not free in t
The most important parts of existentials is how they are used by functions such as myShow.]
-
Can we map OOP interfaces and/or classes to existential types, or are they not quite the same?
-
I'm not quite sure what's meant by "There are no abstract types at runtime" (end of 17.1.2). I feel like you could say the same thing about universal types using the same reasoning, by saying the type given by the client is propagated to the function at runtime. It seems weird to state that abstract types don't exist at runtime when our computation might return a value of abstract type.
[SCW: if you can say this about existentials, you can say it about universals. Both forms have a reduction rule that erases the boundary of type abstraction by substituting a concrete type for a type argument.]
-
How can we define the equality between expressions of abstract types with different implementations? e.g.
D G |- pack natlist with <...> as exists (t. tau) === pack (natlist * natlist) with <...> as exists (t. tau) : exists (t. tau)[SCW: We can't really add a rule to our equational dynamics and still have a compositional definition (i.e. equality defined by the pieces of a term). Instead, we need to go definitions like parametricity or contextual equivalence to be able to define these two expressions as equivalent.]
-
Bob says (end of 17.2) that "the language FE is not a proper extension of F, because existential types (under a lazy dynamics) are definable in terms of universal types." Why the parenthetical caveat? What is it about strict dynamics that inhibits universal types from emulating existential types?
[SCW: this statement depends on what Bob means by "definability". If you consider it to be the property that the dynamic semantics is preserved after translation, then this property is provable for CBN dynamics, but not for CBV dynamics.]
-
On section 17.3 Bob Harper shows how to implement existential types in terms of universal types. He mentions this only works "under a lazy dynamics". If I'm understanding correctly this is how Haskell does it, where we say,
{-# LANGUAGE ExistentialQuantification #-} data ShowList = forall s . Show s => ShowList sI don't understand why this only works under lazy evaluation?
[SCW: Despite the forall keyword, this is not actually defining existentials using universals. Haskell natively supports a form of existential types.]
-
The interface of queue abstraction is given in 17.2. I can use the same interface for stack abstraction. But their behaviours would be different because in case of stack, I shall extract the tail instead of the head by rem. So is it not necessary for the interface to come together with a proof that shows it does what is expected of it?
[SCW: Yes, to show representation independence, you need to show that your implementation respects some relation R in certain ways. For example, we can represent a stack and queue by a list, so the relation R could be the identity function. However this R does not satisfy properties (1)-(3) at the bottom of page 151. Nor is there another relation R that would work.]
-
It seems to me that an interface should be more than just a collection of types. More specifically, an interface should give us some idea about what outputs to expect given certain inputs, and also enforce performance guarantees e.g. for balanced binary trees. Are there languages that are expressive enough to allow for such specifications e.g. if we have an interface for a list that supports insert and remove then we want the specification to force remove(insert(a, l)) = a to be true.
[SCW: Coq can express, for example, that an abstract data structure must satisfy properties such as "remove(insert(a, l)) = a". However, Coq's semantics doesn't talk about the running time, so it can't make restrictions in that respect. There are some type systems that allow you to reason about running time, but none are available in implemented languages.]
-
Why does Bob define bisimulation the way he does, using relations? I would have thought that we might define two implementations of an interface parameterized on a type A to be equivalent if whenever f is a term in the interface of the form
f : for all A. T_1 -> T_2 -> ... -> T_n -> Awith f_1 and f_2 being two different implementations then we have
f_1(t_1, t_2, ..., t_n) = f_2(t_1, t_2, ..., t_n)i.e. whenever a function in the interface computes something of type A, then we get the same thing of type A from both implementations.
[SCW: Your definition of bisimilarity works for expressions of function types, but you need to extend it to define bisimilarity for other types of expressions in the language. The idea of bisimilarity is that it is based on observations: terms are identified if they cannot be distinguished through observation. We observe functions by applying them tyo arguments. We observe existentials by opening them and using them according to their interface.]
-
I think it would be great if we could go through the example carefully, including the part on representation independence.
[SCW: Yes!]