Encoding ExistentialQuantification with RankNTypes

Question

I've read in a few places claims that equivalent functionality to ExistentialQuantification can be had using RankNTypes. Could someone provide an example of why this is or is not possible?

Answer 1

Normally, all type variables in Haskell are implicitly universally quantified at the outermost scope of the type. RankNTypes allows a universal quantifier forall to appear nested, e.g. the type forall a b. (a -> a) -> b -> b is very different from forall b. (forall a. a -> a) -> b -> b.

There is a sense in which types on the left side of a function arrow are logically "negated", in roughly the same sense that (->) is logical implication. Logically, the universal and existential quantifiers are related by a De Morgan duality: (∃x. P(x)) is equivalent to ¬(∀x. ¬P(x)), or in other words "there exists an x such that P(x)" corresponds to "it is not the case that, for all x, P(x) is false".

So a forall on the left of a function arrow is "negated" and behaves like an existential. If you put the whole thing to the left of another function arrow it's double-negated and behaves as a universal quantifier again, modulo some fiddly details.

The same idea of negation applies to values as well, so to encode the type exists x. x we want:

1. forall x. in contravariant (negated) position
2. a value of that type x in covariant (positive) position.

Since the value must be inside the scope of the quantifier, our only choice is double-negation--a CPS transform, basically. To avoid restricting things otherwise, we'll then universally quantify over the type on the right of the function arrows. So exists x. x is translated to forall r. (forall x. x -> r) -> r. Compare the placement of the types and quantifiers here to the requirements above to verify that it meets the requirement.

In more operational terms this just means that given a function with the above type, because we give it a function with a universally quantified argument type, it can apply that function to any type x it likes, and since it has no other way of getting a value of type r we know it will apply that function to something. So x will refer to some type, but we don't know what--which is basically the essence of existential quantification.

In more practical, day to day terms, any universally quantified type variable can be regarded as existential if you're looking at it from the "other side" of a function type. Because the unification performed as part of type inference transcends quantifier scope, you can sometimes end up in a situation where GHC would have to unify a type variable in an outer scope with a quantified type from a nested scope, which is how you get compiler errors about escaping types and skolems and whatnot, the latter (I assume) being related to Skolem normal form.

The way this relates to data types using existentials is that while you can declare a type like this:

data Exists = forall a. Exists a

That represents an existential type, to get at the "existential type" you need to unwrap it by pattern matching:

unexist :: Exists -> r
unexist (Exists x) = foo x

But if you consider what the type of foo would have to be in this definition, you end up with something like forall a. a -> r, which is equivalent to the CPS-style encoding above. There's a close relationship between CPS transforms and Church encoding of data types, so the CPS form can also be seen as a reified version of the pattern match.

Finally, relating things back to logic--since that's where the term "existential quantifier" comes from--note that, if you think of being left of an arrow as negation and kinda squint to ignore the forall r. ... CPS cruft, these encodings of existential types are exactly the same thing as the De Morgan dualized form ¬(∀x. ¬P(x)) that was the starting point. So these really all are just different ways of looking at the same concept.