I'm talking about first-order existential types, as summarized here, with pack as the introduction form that bundles up a type with an expression of that type, and open as the elimination form that unpacks the type and its representative expression.

This seems just as fundamental as parametric polymorphism (universal types), so I'm surprised that this construct isn't implemented in e.g. Haskell or OCaml. Does anyone know the reasons for this?

  • 1
    $\begingroup$ More details are needed. When one says existential type do they not mean a witness and a proof that the witness satisfies some property? If so, what is a "proof" in imperative/OO languages? $\endgroup$ – Musa Al-hassy Nov 8 '16 at 21:12
  • 2
    $\begingroup$ @MusaAl-hassy: No, they do not mean that, see stackoverflow.com/questions/292274/what-is-an-existential-type $\endgroup$ – Andrej Bauer Nov 8 '16 at 21:48
  • $\begingroup$ Learning things is a delight! Now I've more enjoyable articles to read; Thanks Andrej! $\endgroup$ – Musa Al-hassy Nov 9 '16 at 14:28
  • $\begingroup$ Here is a bit of explanation to the less sophisticated readers who may want to understand the comments here. Constructively, we convince others that $\exists x.\varphi(x)$ holds if we can show an example (i.e., witness) $a$ and present an argument that $\varphi(a)$ holds. In some settings, we can consider types as logical statements, and terms as proofs to those statements. That is the background of Al-hassy's question. One possible choice of further reading may be Paul Taylor's Practical Foundations of Mathematics, Section 2.4. $\endgroup$ – Yuning Feb 5 at 14:09
  • $\begingroup$ Nevertheless, for the moment very few real-life programming languages possess such immediate correspondence to logic. Typed functional languages are usually good approximations, while imperative/OO languages are probably too far apart. For that reason witness-proof is technically not a way to think of `existential types' in imperative languages. However, forming and using existential types there involve a type $a$ and a value of type $\varphi(a)$ in a similar way. So to a programmer trying to express abstraction in their data and code, the mechanism is similar. $\endgroup$ – Yuning Feb 5 at 14:19

OCaml's idea of modules roughly correspond with existential types ;)

Let's set up some rough semantics in order to frame this correspondence properly. First, I'll give the intro/elimination rules for existential types (I'll only use a variable $\to$ type context $\Gamma$ for the sake of simplicity here): $$ \frac{\Gamma \vdash e\{\alpha\mapsto \tau\} : \sigma\{\alpha\mapsto \tau\}}{\Gamma \vdash [\tau, e] : \exists \alpha. \sigma} ({\rm Pack}) ~~~~~~~ \frac{\Gamma \vdash e : \exists \alpha.\sigma ~~~ \Gamma, x:\sigma \vdash e' : \tau'}{\Gamma \vdash {\rm let} ~ [\alpha, x] = e ~ {\rm in} ~ e' : \tau'}({\rm Unpack}) $$ where $e\{\alpha \mapsto \tau\}$ substitutes all occurrences of the type variable $\alpha$ with the concrete type $\tau$. In practice, we will also decorate the packed form with its existential type in order to disambiguate the semantics.

Operationally, we have the context reductions: $$ \frac{e \Downarrow v}{[\tau, e] \Downarrow [\tau, v]} ~~~~~~ \frac{e \Downarrow v}{{\rm let} ~ [\alpha, x] = e ~ {\rm in} ~ e' \Downarrow {\rm let} ~ [\alpha, x] = v ~ {\rm in} ~ e'} $$ which corresponds to the reduction strategies that reduces the expressions in the existential packages and the expressions to be unpacked.

Finally, we have the extensional $\eta$-reduction rule: $$ \frac{}{{\rm let} ~ [\alpha, x] = [\tau, v]_{\exists \alpha. \sigma} ~ {\rm in} ~ e \to e \{\alpha \mapsto \tau, x \mapsto v\}} $$

So for example, the program \begin{align*} {\rm let} ~ [\alpha, x] &= [{\rm int}, (0, {\rm succ})]_{\exists \alpha. \alpha \times (\alpha \to \alpha)} ~ {\rm in} ~ ({\rm snd} ~ x : \alpha \to \alpha)({\rm fst} ~ x : \alpha)\\ &\to^{\eta} ({\rm snd} ~ (0, {\rm succ}) : {\rm int} \to {\rm int})({\rm fst} ~ (0, {\rm succ}) : {\rm int}) \\ &\to^* {\rm succ} ~ 0 \\ &\to^\beta 1 \end{align*}

This exact idea is present in OCaml's concept of modules, save that the packed type must be a record (but which can be made to be isomorphic to any other OCaml type). For example, the creation of an existential type is done through the module type keyword:

module type Bundle =
  type α
  val data : α * (α -> α)

This signature corresponds to the existential type $\exists \alpha. \alpha \times (\alpha \to \alpha)$. We can witness an inhabitant of this type by instantiating it with the struct keyword:

module BundleInt : Bundle = struct
  type α = int
  val data = (0, (+) 1)

which corresponds to the pack/intro $[{\rm int}, (0, (+) 1)]_{\exists \alpha. \alpha \times (\alpha \to \alpha)}$. Unfortunately, there is no explicit ${\rm let} \dots$ elimination form, but something like open BundleInt is equivalent to let [α, data] = BundleInt in ... where α and data are specified in the creation of the module type Bundle.

So while module types aren't exactly the same as your traditional existential types (the variables to be bound are explicitly pushed into the intro-form rather than in the elimination-form), their expressiveness are the same.

  • 1
    $\begingroup$ For some reason I don't remember seeing this answer, but thanks nonetheless! There actually is an let open construct in OCaml which seems to have nearly the same semantics as unpack. That said, there is one point I disagree with; you say that they're equally expressive, but with existential types, you can write a function parameterized by an existential type, whereas in OCaml you can't (you have to write functors parameterized by modules). $\endgroup$ – gardenhead Jan 27 '17 at 5:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.