Existential types in C# - Part 3
Tags: csharp, dotnet, functional
Published: 2020-03-19 04:54:41

# Recap

In a previous [article](https://dev.to/shimmer/c-generic-type-brainteaser-2lk1), 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](https://dev.to/shimmer/existentially-quantified-types-in-c-part-2-3jkp) 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](https://dev.to/shimmer/continuation-passing-style-in-c-1k6c) (CPS), which is akin to logical double-negation via the [Curry-Howard correspondence](https://dev.to/shimmer/the-curry-howard-correspondence-3obh). 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`[^1], 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](https://dev.to/shimmer/the-curry-howard-correspondence-3obh) 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](https://github.com/nickcowle/Talks/blob/master/Existentials%20-%20Playing%20Hide%20and%20Seek%20With%20Your%20Types.pdf)
  * [Initial Algebras for the Uninitiated](https://github.com/nickcowle/Talks/blob/master/Initial%20Algebras%20for%20the%20Uninitiated.pdf)
  * [Squeezing More Out of the F# Type System – Introducing Crates](https://www.gresearch.co.uk/article/squeezing-more-out-of-the-f-type-system-introducing-crates/)
  * [TypeShape](https://eiriktsarpalis.github.io/typeshape/#/16)
* Universally quantified types:
  * [First-class polymorphism](http://mlton.org/FirstClassPolymorphism)
* Stack Exchange questions:
  * [What is an existential type?](https://stackoverflow.com/questions/292274/what-is-an-existential-type)
  * [How can an existential type be defined in terms of universal type?](https://cs.stackexchange.com/questions/113452/how-can-an-existential-type-be-defined-in-terms-of-universal-type)
  * [Universal and existential types
](https://cstheory.stackexchange.com/questions/32515/universal-and-existential-types)
* Haskell, first-order logic, and C-H correspondence:
  * [Existential type-curry](http://blog.ezyang.com/2010/10/existential-type-curry/)
  * [Existential types and data abstraction](http://iveselov.info/posts/2012-08-30-existential-types.html)

[^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>`.