Domain Theory and Polymorphism

Question

Domain theory gives an amazing theory of computability in the presence of simple types. But when parametric polymorphism is added there doesn't seem to be a nice theory that explains whats going on quite as nicely as domain theory explains computation over simple types. Certainly I wouldn't expect such a thing to exist for System-F because no set theoretic models of System-F exist. What about a restriction of System-F that has predictive and has a universe hierarchy? Has this been studied? Is there a nice domain theory that applies to it? Going further what about dependent types? Can domain theory somehow be mixed with weak $\omega$-groupoids to accomplish something?

Answer 1

There are many ways to model polymorphism via domain theory, let me just describe one that is easy to understand, so you can think about it yourself. It's a "PER model".

Take any model of the untyped $\lambda$-calculus, for instance a domain $D$ such that $D \to D$ is a retract of $D$ (for instance, take $D$ such that $D \cong \mathbb{N}_\bot \times (D \to D))$. Let $\Lambda : D \to (D \to D)$ and $\Gamma : (D \to D) \to D$ be the retraction and the section, respectively.

We are going to interpret the types as partial equivalence relations (PER) on $D$. Recall that a PER is a relation which is symmetric and transitive, but it need not be reflexive. To each type $\tau$ we thus assign a PER $\sim_\tau$. Think of $x \sim_\tau x$ as "$x$ is an element of $\tau$" and $x \sim_\tau y$ as "$x$ and $y$ are equal as far as $\tau$ is concerned".

We can have some basic types (but need not), for instance if we make sure that $\mathbb{N}_\bot$ is a subdomain of $D$ via an embedding $\iota : \mathbb{N} \to D$ then we may define $\sim_\mathtt{nat}$ by $$x \sim_\mathtt{nat} y \iff \exists n \in \mathbb{N} . x = \iota(n) = y.$$

Given PERs $\sim_\tau$ and $\sim_\sigma$, define the function space PER $\sim_{\tau \to \sigma}$ by $$x \sim_{\tau \to \sigma} y \iff \forall z, w \in D . z \sim_\tau w \Rightarrow \Lambda(x)(z) \sim_\sigma \Lambda(y)(w)$$

The terms are interpreted as untyped $\lambda$-calculus terms as one would normally interpret them in $D$.

Here's the punchline. You may interpret polymorphism as intersection of PERs, that is: $$x \sim_{\forall X. \tau(X)} y \iff \text{for all PERs $\approx$, $x \sim_{\tau(\approx)} y$}. $$ We can caclulate the PER corresponding to $\forall X. X$: it is the intersection of all PERs, but that is going to be the empty PER. Calculating $\forall X . X \to X$ is an interesting exercise. Calculating $\forall X . X \to X \to X$ is a difficult exercise (which kept me busy for a week when I was a student of domain theory).

If we want recursion in our language then we need to account for fixed points. One possibility is to restrict PERs to those which contain $\bot_D$ and are closed under suprema of increasing chains. More precisely, take only those PERs $\approx$ for which

• $\bot_D \approx \bot_D$, and
• if $x_0 \leq x_1 \leq x_2 \leq \cdots$ and $y_0 \leq y_1 \leq y_2 \leq \cdots$ are increasing chains in $D$ such that $x_i \approx y_i$ for all $i$, then $\sup_i x_i \approx \sup_i y_i$.

We can now interpret $\mathtt{fix}_{\tau} : (\tau \to \tau) \to \tau$ by applying the Kanster-Tarski theorem about existence of fixed points, just like we do in ordinary domain theory. This time, $\forall X . X$ is not empty, as it contains precisely $\bot_D$.

Answer 2

Roy Crole gives a nice explanation of how to use domain theory to model type polymorphism in his book Categories for Types, specifically in section 5.6.