Recap

In a previous article, we saw how to emulate first-class polymorphism by encapsulating a generic type in a non-generic interface. This technique allows us to control the scope of a universally quantified type variable.

We then saw an example of emulating an existential type in C# using generics. There are two steps:

1. Use the encapsulation technique described above to wrap the hidden type in a "carton". In our example, we created IListCarton to hide IList<TItem>.

2. Create a callback interface then allows access to the value hidden inside the existential ("inversion of control"). We called this callback an "operation". For example, IListOperation<TReturn> allows operations on hidden instances of IList<TItem>.

In this article, I'd like to walk through the type theory that establishes the equivalence between this emulation technique and a true existential type. This is purely background information, and is not at all necessary for anyone who wants to use the technique.

Continuation passing style

We've talked before about a programming technique called continuation passing style (CPS), which is akin to logical double-negation via the Curry-Howard correspondence. If you have a value of type T that you don't want to expose directly, you can instead convert to CPS by implementing a function of type (T -> TRet) -> TRet¹, where T -> TRet is a continuation (i.e. a callback function). In English, this means that if you have a hidden instance of T and you are given a T -> TRet continuation, you can produce a TRet.

If we make the universal quantification explicit, we get the following approximate equivalence:

T ≅ ∀TRet.((T -> TRet) -> TRet)

This just says that we can emulate a given type, T, if, for any continuation returning type TRet, we can actually produce a TRet. Next, let's see what happens when we plug in an existential type, such as ∃TItem.IList<TItem>, for T:

∃TItem.IList<TItem> ≅ ∀TRet.(((∃TItem.IList<TItem>) -> TRet) -> TRet)

First-order logic

We can use the Curry-Howard correspondence to think about this as a logical expression, rather than as a type.

There's a neat logical equivalence that comes in handy at this point:

∃x.A(x) → B ≡ ∀x.(A(x) → B)

The left side says that the existence of an x that makes proposition A(x) true also implies that proposition B is true. The right side says that any x that makes A(x) true also makes B true. Intuitively, I think this is fairly clear, but it can also be rigorously proved.

We can use this equivalence to convert our existential quantifier to a universal quantifier:

∃TItem.IList<TItem> ≅ ∀TRet.(((∃TItem.IList<TItem>) -> TRet) -> TRet)
∃TItem.IList<TItem> ≅ ∀TRet.((∀TItem.(IList<TItem> -> TRet)) -> TRet)

For clarity, the universal quantifiers can omitted (but are still implied):

∃TItem.IList<TItem> ≅ (IList<TItem> -> TRet) -> TRet

This means that we can emulate an existential type using CPS, the same we can emulate any other type. This makes intuitive sense: Since CPS can be used to hide any type, we can use it to hide the type contained inside an existentially quantified type.

Since we have two inner types, TItem and TRet, we need a separate interface for each one in turn: IListCrate allows a caller to specify TRet and then IListOperation<TRet> allows a caller to specify TItem for any TRet. This gives us the full C# implementation.

Additional resources

For anyone wanting to dig deeper, here's a list of articles that I used in preparing this series on universal and existential types in C#:

• F# (G-Research):
  • Existentials - Playing Hide and Seek With Your Types
  • Initial Algebras for the Uninitiated
  • Squeezing More Out of the F# Type System – Introducing Crates
  • TypeShape
• Universally quantified types:
  • First-class polymorphism
• Stack Exchange questions:
  • What is an existential type?
  • How can an existential type be defined in terms of universal type?
  • Universal and existential types
• Haskell, first-order logic, and C-H correspondence:
  • Existential type-curry
  • Existential types and data abstraction

1. I've converted to F# syntax here because it's easier to understand than C#. (T -> TRet) -> TRet is the same as Func<Func<T, TRet>, TRet>. ↩