8
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ I'm confused: there are domain-theoretic models of the untyped $\lambda$-calculus, which intuitively is a typed calculus with a type $\alpha\simeq\alpha\rightarrow\alpha$. This, of course, has no models in sets either. Why would you expect there to be no domain models of system F? Have you tried searching online? $\endgroup$ – cody Nov 22 '16 at 20:42
  • $\begingroup$ I understood that there are no models of system F in which functions are interpreted as any kind of function in set theory. I understood there to be no "naive" set theoretic models of the typed lambda calculus but that set theoretic models exist as long as the functions are continuous functions. Then much like the continuous real functions have the same cardinality as the reals so too can the scott-continuous functions have the same size as their (co)domain. I understood this to be how the size problem was resolved. I understood such a solution to not exist for system-F however. $\endgroup$ – Jake Nov 22 '16 at 20:55
  • $\begingroup$ I should also add that I understood domain theory to still be set theoretic in principal. That is functions are still set theoretic functions it's just that you only become concerned with the continuous functions when interpreting functions in a calculus. Hence my understandings seem to rule out System-F fitting into a domain theoretic model. Perhaps it is one of my understandings that is wrong here. $\endgroup$ – Jake Nov 22 '16 at 21:07
  • 3
    $\begingroup$ I see, thanks for your clarifications. The most "domain-theory-like" treatment of system F I know of is Girard's "Coherent Spaces" the treatment of which is outlined here by Paul Taylor. I don't know if this is a "nice theory" as per your request, but to be honest, I don't really see domain theory as being that nice in general for semantics of total languages... $\endgroup$ – cody Nov 22 '16 at 21:12
  • 1
    $\begingroup$ @cody: tsk, tsk. $\endgroup$ – Andrej Bauer Jun 10 '17 at 12:30
5
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ This is a beyond fantastic answer! This basically gives the same tools that parametricity gives us and the tools of domain theory. This is exactly what I was looking for. Well, I've got something to do this weekend now. $\endgroup$ – Jake Jun 10 '17 at 13:36
  • $\begingroup$ For the record, I learned this stuff from Dana Scott. I am pretty sure John Reynolds knew about PER models by the time he invented parametricity. I always thought that parametricity came from PER models, anyhow. $\endgroup$ – Andrej Bauer Jun 10 '17 at 13:46
  • $\begingroup$ I had it in my head that he was your advisor. Is this written down anywhere or is this folklore? $\endgroup$ – Jake Jun 10 '17 at 13:47
  • $\begingroup$ There's lots of stuff written down about this. What are you looking for? The first historic paper (which would be by Dana Scott), a classic paper that gets things really going, a textbook? $\endgroup$ – Andrej Bauer Jun 10 '17 at 13:50
  • 2
    $\begingroup$ The textbook Domains and Lambda Calculi by Roberto Amadio and Pierre-Louis Curien covers PER models in Chapter 15, and a PER model of System F in 15.2. $\endgroup$ – Andrej Bauer Jun 10 '17 at 17:53
0
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ Could you at least summarize that section for the benefit of people who might not have the book? A paragraph or two giving the main ideas would be plenty. $\endgroup$ – David Richerby Jun 9 '17 at 20:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.