From System F to Curry-Howard: Encoding ∃ with nothing but ∀.
Rank-2 polymorphism is one of GHC’s most elegant extensions, bridging the gap between Hindley-Milner and System F. While its surface purpose is to allow functions to accept polymorphic arguments, its deeper significance lies in the Curry-Howard correspondence: with a simple continuation-passing-style (CPS) transformation, the universal quantifier ∀ can encode the existential quantifier ∃. This article explores Rank-2 types in Haskell, their practical applications, and the logical duality that lets us pack and unpack existentials using nothing but nested foralls.
The Rank of a Type
In standard Haskell98, all polymorphism is Rank-1 (or prenex): every ∀ sits at the outermost level of the type signature. The rank of a type measures how deeply a polymorphic type is nested to the right of a function arrow.
| Rank | Description | Example |
|---|---|---|
| Rank-0 | Monomorphic (no ∀) | Int, Bool -> Int |
| Rank-1 | Standard Haskell98 polymorphism | ∀a. a -> a (written a -> a) |
| Rank-2 | ∀ appears to the right of an arrow | (∀a. a -> a) -> (Int, Bool) |
| Rank-N | ∀ nested arbitrarily deep | (∀a. a -> a) -> (∀b. b -> b) |
We enable higher-rank types with:
{-# LANGUAGE RankNTypes #-}This extension subsumes the older Rank2Types; it allows ∀ to appear anywhere in the type tree, not just at the top level.
-- Rank-2: the parameter f itself is polymorphic
rank2Example :: (∀ a. a -> a) -> (Int, Bool)
rank2Example f = (f 42, f True)
-- Rank-1 (fails): `a` is unified once by the caller
badExample :: (a -> a) -> (Int, Bool)
badExample f = (f 42, f True) -- ERROR: a cannot be both Int and BoolThe parentheses around ∀ a. a -> a are essential. Without them, the quantifier would scope over the entire arrow, yielding the same Rank-1 type as badExample.
The crucial difference between Rank-1 and Rank-2 is the locus of control for type instantiation:
Rank-1 ∀a. a -> a: The caller instantiates a. The callee is polymorphic and must work for whatever type the caller supplies.
Rank-2 (∀a. a -> a) -> (Int, Bool): The callee (the function body) instantiates a. The caller must supply a function that works for all types, and the callee may apply it at many different types.
| Feature | Rank-1 (a -> a) | Rank-2 (∀a. a -> a) |
|---|---|---|
| Type choice | Caller chooses a | Callee chooses a |
| Applicability | Applied at one type | Applied at many types |
| Actual argument | Monomorphic function (Int -> Int) | Polymorphic function (id) |
Practical Motivations for Rank-2
Before diving into the logical machinery, let us see why Rank-2 types are useful in practice.
Rank-1 polymorphism lets a function produce a polymorphic value. Rank-2 lets a function consume one:
withUniversal :: (∀ a. Show a => a -> String) -> String
withUniversal showFunc = showFunc 123 ++ showFunc True
main :: IO ()
main = putStrLn $ withUniversal show -- OK: show :: ∀a. Show a => a -> StringHere the caller must hand over a genuinely polymorphic function. A monomorphic Int -> String would be rejected.
One of the most celebrated uses of Rank-2 is runST, which isolates mutable state:
runST :: (∀ s. ST s a) -> aBecause the ∀ s sits in the argument position, the caller must produce an ST action valid for every possible state token s. Consequently, no reference of type STRef s a can escape the scope of runST—it would require a specific s to exist outside, which is impossible. This is the type-system guarantee that makes the pure-functional ST monad safe.
Rank-2 is also the theoretical foundation for existential types. In GHC we can write:
{-# LANGUAGE ExistentialQuantification #-}
data SomeShowable = ∀ a. Show a => MkSome aThis declaration says: "there exists some type a such that we have a value of type a and a Show instance for it." The concrete type is hidden inside the constructor.
What is less obvious is that we do not need a separate exists keyword at all. We can encode the very same abstraction using only forall and Rank-2.
The Logical Bridge: Universals and Existentials
Under the Curry-Howard isomorphism, types are propositions and programs are proofs. The universal quantifier ∀ corresponds to parametric polymorphism. The existential quantifier ∃ corresponds to abstract data types, modules, and information hiding.
In classical logic, ∃ and ∀ are dual:
Classically one can relate them via double negation, but in constructive (intuitionistic) logic we use a CPS-style encoding:
\[\exists a. P(a) \quad \cong \quad \forall r. (\forall a. P(a) \to r) \to r\]This is the Rank-2 encoding of existential types.
Left side: "There exists a type a and a proof/value of P(a)."
Right side: "For every possible result type r, if you give me a handler that can consume a P(a) for any type a, I will produce an r."
Why are these equivalent? Because the only way the implementation can fulfill its promise of producing an arbitrary r is to invoke the handler with some concrete, hidden P(a). The existence of that hidden a is forced by the type.
Existentials as Rank-2 CPS in Haskell
Let us make the encoding concrete.
{-# LANGUAGE ExistentialQuantification #-}
data SomeP = forall a. MkSome (P a){-# LANGUAGE RankNTypes #-}
type SomeP' = forall r. (forall a. P a -> r) -> r
-- Construction (packing)
mkSome :: P a -> SomeP'
mkSome pa = \k -> k pa -- k :: forall a. P a -> r
-- Elimination (unpacking)
runSome :: SomeP' -> (forall a. P a -> r) -> r
runSome some k = some kNotice that forall itself never changes its meaning. Both occurrences of forall still mean "for all." What changes is the polarity (the position in the type tree) and the CPS structure built around them.
forall| Position | Type Fragment | Role | Control |
|---|---|---|---|
Inner forall a | P a -> r | Forces the handler k to be parametric in a. The eliminator cannot know what a is. | Caller (eliminator) must be generic. |
Outer forall r | (… -> r) -> r | Quantifies the result type, making the encoding independent of any specific return type. | Caller chooses r; the box promises to deliver it. |
The inner forall a is the engine of information hiding. Because k must work for all a, it cannot perform any type-specific operation (like +1 on an Int or length on a list). It can only use the interface provided by P.
The outer forall r is the engine of logical completeness. It guarantees that the existential can be eliminated to any conclusion that does not depend on the hidden witness.
Why the Encoding Works: Proof Obligations and Parametricity
In constructive logic, to prove ∃a. P(a) you must produce a witness—a concrete type w and a value p : P(w). Let us walk through the two directions of the equivalence.
Assume we have a witness: a concrete type w and a value p :: P w.
To prove ∀r. (∀a. P a -> r) -> r, we must show that for any target type r and any handler k :: ∀a. P a -> r, we can produce an r.
Simply apply k at w:
k w p -- :: rBecause k is parametric, it accepts any type a, including our hidden w. This is exactly what mkSome does.
Assume we hold a value of type ∀r. (∀a. P a -> r) -> r. How do we know there is really some P(a) hidden inside?
The key observation is that the implementation has only one way to produce an r: it must call the handler k. And when it calls k, it must supply some concrete P(a). The choice of which a to use belongs to the implementation (the "proponent" in game-semantics terms), not to the caller.
If the implementation had nothing inside, it could not construct an arbitrary r. You, the caller, could demand r = Void (or any uninhabited type), and the implementation would be stuck. The very ability to answer every possible r forces the existence of a hidden witness.
Universal ∀: The opponent (the environment, the caller) chooses the type instance.
Existential ∃: The proponent (the program, the constructor) chooses the type instance.
In the Rank-2 encoding, the inner forall a sits in a negative position (to the left of an odd number of arrows). This flips the polarity: the caller must move first by supplying a generic k, and then the implementation gets to choose the concrete a when invoking k. The nested forall thereby transfers the choice of type from caller to callee, achieving existential behavior with universal syntax.
The Outer forall r: Logical Completeness
A common question is: why do we need the outer quantifier? Why not simply:
type BadExists P = (forall a. P a -> Int) -> IntThe answer spans logic, abstraction, and practical expressiveness.
In natural deduction, the elimination rule for ∃ is:
Meaning: if you know ∃a. P(a) and you can prove some conclusion Q from the assumption that you hold an arbitrary P(a)—provided Q does not mention a—then Q follows.
Crucially, Q is arbitrary (as long as it is independent of a). The outer forall r encodes exactly this: r plays the role of Q, and the condition a ∉ FV(Q) is enforced by the scope rules of the type system (r is chosen outside the scope of a).
The purpose of an existential is type abstraction.
The constructor knows the witness type (e.g., Int).
The eliminator does not.
If the eliminator could only unpack the box into a fixed type like Int, the abstraction boundary would leak information: the box would behave like a secret Int. By allowing the eliminator to choose any r, we ensure that the constructor’s choice of witness and the eliminator’s choice of result are completely decoupled. This is the hallmark of proper information hiding.
Imagine a safe that hides its contents.
Compiler CPS is like a courier who asks, "Where should I drop this package?" The destination (r) is fixed—your front door. The courier merely makes the delivery flow explicit.
Existential CPS is like a magic safe. You say, "I am ready to process whatever is inside, and I will tell you the destination." The safe can be opened at the office, at home, or in a warehouse—any r—and the safe’s owner (the constructor) decides what item (a) to hand over. The outer forall r makes the safe portable; the inner forall a makes its contents opaque.
Category-Theoretic Perspective
In category theory, quantifiers arise as adjoints to the "diagonal" or "application" functor:
Universal ∀ is the right adjoint.
Existential ∃ is the left adjoint.
They are distinct, yet related through the co-Yoneda lemma:
\[\exists a. F(a) \times (a \to r) \cong F(r)\]When F is the identity functor, this becomes:
which is precisely the structural essence of our CPS encoding. The forall in Haskell behaves as a categorical end (a limit), yet when placed in the negative position of a continuation, it encodes a co-end (a colimit), i.e., an existential.
This is the deep reason why no separate exists primitive is required in System F: the expressive power of parametric polymorphism (∀) is sufficient to simulate both limits and colimits.
Distinguishing Two Common Rank-2 Patterns
Not every Rank-2 type is an existential in disguise. It is important to keep two patterns separate:
| Form | Meaning | Control |
|---|---|---|
(forall a. P a) -> Q | Accept a polymorphic processor. The caller provides universal capability. | Caller must be generic. |
forall r. (forall a. P a -> r) -> r | Encode an existential. The implementation hides a specific type. | Callee chooses the witness. |
The first is a "genuine" nested universal: the function demands a value that works for all types. The second uses the same forall keyword, but the CPS wrapping and the negative position turn it into an existential container.
Putting It All Together: A Complete Example
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
-- | A type constructor for our predicate P.
type P a = (a, a -> String)
-- === Direct existential ===
data Box = forall a. MkBox (P a)
-- === Rank-2 CPS encoding ===
type Box' = forall r. (forall a. P a -> r) -> r
-- Packing
mkBox :: P a -> Box'
mkBox pa = \k -> k pa
-- Unpacking
runBox :: Box' -> (forall a. P a -> r) -> r
runBox box k = box k
-- Usage
example :: IO ()
example = do
let boxInt = mkBox (42, \x -> "Int: " ++ show x)
let boxBool = mkBox (True, \x -> "Bool: " ++ show x)
-- Eliminate to String
let s1 = runBox boxInt (\(x, f) -> f x)
putStrLn s1 -- prints "Int: 42"
-- Eliminate to the *same* box, but to IO ()
runBox boxBool (\(x, f) -> putStrLn (f x)) -- prints "Bool: True"Notice how boxInt and boxBool hide their internal types, yet can be eliminated to any result type r the caller desires.
Conclusion
Rank-2 polymorphism is far more than a syntactic convenience. It is the doorway through which Haskell escapes the confines of Hindley-Milner and enters the full expressive power of System F.
The key insights are:
forall never changes its meaning. It always means "for all."
Polarity is what matters. When forall appears in a negative position (as a function argument), control over type instantiation flips from caller to callee.
CPS completes the picture. The outer forall r and the continuation structure (… -> r) -> r create a logically complete encoding of existential quantification.
Information hiding is parametricity. The inner forall a forces the eliminator to be blind to the witness type, which is exactly the guarantee we need for abstract data types.
Whether you are using runST to isolate state, building heterogeneous containers, or reasoning about types through the Curry-Howard lens, Rank-2 polymorphism provides the essential bridge between the universal and the existential—proving once again that in the lambda calculus, everything is a function, even a hidden type.
Types and Programming Languages (Pierce) — Chapters on System F and existential types.
The Implementation of Functional Programming Languages (Peyton Jones) — Early discussion of Rank-2 and Rank-N types.
Reynolds, J. C. — Polymorphism is not set-theoretic.
Plotkin, G. D. — Call-by-name, call-by-value and the λ-calculus (foundations of CPS).
GHC User’s Guide — RankNTypes, ExistentialQuantification, ImpredicativeTypes.