3
$\begingroup$

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?

$\endgroup$
  • 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
4
$\begingroup$

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 =
sig
  type α
  val data : α * (α -> α)
end

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)
end

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.

| cite | improve this answer | |
$\endgroup$
  • 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.