existential.md

This document explores the relationship between module systems, existential types and abstract data types for non-experts of type theory. I wrote this mainly to clarify my understanding of how a combination of these three leads to the development of modular programming. The theoretical part of this document is adapted from [TAPL-Pierce], and hopefully simplified enough for understanding.

Existential Types

In theory an existential type is written as $\{ \exists X,T \}$. The operational intuition is that an element of $\{ \exists X,T \}$ is a pair, written $\{ *S, t \}$, of a type $S$ and a term $t$ of type $[ X \rightarrow S ]T$.

Well that looks like a mouthful - let's deconstruct a bit with some analogy with actual examples.

The pair $\{ *S, t \}$ actually denotes a package or module in our program, with one type component and one term component. The type component $S$ is the hidden representation type and the term component $t$ consists of the rest of the package. As an example the package $p = \{ *Nat, \{a = 5, f = \lambda x:Nat, succ(x) \}\}$ has the existential type $\{ \exists X,\{a:X, f:X \rightarrow X\} \}$. The hidden type here is $Nat$ which is the representation type hidden within the package and the term (or value) component is a record containing a field $a$ of type $X$ and a field $f$ of type $X \rightarrow X$, for some $X$ (namely $Nat$).

Abstract Data Types

Based on the definition of abstract data types in [TAPL-Pierce], a conventional abstract data type (ADT) consists of:

1. a type name $A$
2. a concrete representation type $T$
3. implementation of some operations for creating, querying and manipulating values of type $T$, and
4. an abstraction boundary enclosing the representation and operations

Here's a concrete example of an ADT in OCaml, a module for a Counter.

module type Counter = sig
  type t
  
  val make: int -> t
  val inc : t -> int -> t
  val get : t -> int
end

module IntCounter : Counter = struct
  type t = int
  
  let make initial_value = initial_value
  let inc counter increment = counter + increment
  let get counter = counter
end

The above package declares the following:

1. a module signature, Counter, or a specification of what values/types the module should contain. This signature says that a Counter module should contain some type t as well as three functions of various types. Based on the above definition, the abstract type name of the ADT is Counter.
2. a module implementation, IntCounter, that adheres to the specified signature and uses a concrete representation type int. And the implementations of the operations that deal with Counter objects concretely as ints.
3. the abstraction boundary that spans across the signature and the definition of the module. Beyond this abstraction boundary, the association between Counter and int is broken, so that the only thing that can be done with a counter.make is to use it as an argument to counter.inc and counter.get.

A key property of such information hiding is representation independence. We can substitute an alternative implementation of the Counter ADT, for example one where the internal representation is a record containing an int rather than just the int.

module RecordCounter: Counter = struct
  type t = { x : int }
  let make (n : int) : t = {x = n}
  let inc (ctr : t) (n : int) : t = {x = ctr.x + n}
  let get (ctr : t) : int = ctr.x
end

Abstract Data Types as Encoding of Existential Types

Based on our definition above, an existential type is a pair, written $\{ *S, t \}$, of a type $S$ and a term $t$ of type $[ X \rightarrow S ]T$. Now take a look at the module declarations for the Counter in the previous section. The signature Counter is the type component and the structure IntCounter or the RecordCounter form the term component of the existential.

Existential Types - Introduction Form

Let's discuss a bit about how to build (or introduce) elements that inhabit existential types. It may be easier to think in terms of how we can package existential types formally.

Consider the existential package that we introduced in the first section along with the definition of existential types. The package $p = \{ *Nat, \{a = 5, f = \lambda x:Nat, succ(x) \}\}$ has the existential type $\{ \exists X,\{a:X, f:X \rightarrow X\} \}$. The type compone t of $p$ is $Nat$ and the value component is a record containing a field $a$ of type $X$ and a field $f$ of type $X \rightarrow X$, for some $X$ (namely $Nat$).

Now we can also say that this same package $p$ can also have type $\{ \exists X,\{a:X, f:X \rightarrow Nat\} \}$, since its right hand component is a record with fields $a$ and $f$ of type $X$ and $X \rightarrow Nat$, for some $X$ (namely $Nat$).

So, how does the type checker automatically decide on the exact type of this existential package ? It can't - hence the programmer must specify which one is intended. And the simplest way to do this is just to add an annotation to every package that explicitly gives its intended type. This is how the full introduction form of existential types will look like:

$$ p = \{ *Nat, \{a = 5, f = \lambda x:Nat, succ(x) \}\} \hspace{.2cm} as \hspace{.2cm} \{ \exists X,\{a:X, f:X \rightarrow X\} \}; $$

The introduction form is also known as pack meaning the packaging of the package.

Existential Types - Elimination Form

The dual form of introduction is elimination, which is also known as the unpack and refers to the open or import directive. It allows the components of the module to be used in some other parts of the program, but holds abstract the identity of the module's type component (look at the discussion on representation independence in the section of ADTs).

Consider our usual example of the existential package $p = \{ \exists X,\{a:X, f:X \rightarrow Nat\} \}$. The elimination form for $p$ will be

$$ let \hspace{.2cm} \{X, x\}=p \hspace{.2cm} in \hspace{.2cm} (x.f \hspace{.2cm} x.a); $$

and it will correspond to module usage in OCaml.

References

1. [TAPL-Pierce] Types and Programming Languages - Benjamin C. Pierce