patternMinor
Domain Theory and Polymorphism
Viewed 0 times
theorypolymorphismanddomain
Problem
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?
Solution
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
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$.
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$.
Context
StackExchange Computer Science Q#66300, answer score: 6
Revisions (0)
No revisions yet.