1
$\begingroup$

In Practical Foundations for Programming Languages, on page 138 (page 156 of the pdf), it says:

Requiring solutions to all type equations may seem suspicious, because we know by Cantor’s Theorem that an isomorphism such as $X \cong (X \rightarrow \mathbf{2})$ is set-theoretically impossible. This negative result tells us not that our requirement is untenable, but rather that types are not sets.

I understand why solving such an isomorphism is set-theoretically impossible, and therefore why being able to solve it means that "types are not sets". However, I cannot think of any possible type $X$ that would actually solve this isomorphism.

Can anyone give an example of such a type (and ideally, some advice for more generally solving such type isomorphisms)?

$\endgroup$
  • 1
    $\begingroup$ Note that several functional programming languages would accept recursive type definitions. E.g. you can define lists in Haskell using data List a = Nil | Cons a (List a). You can also write data X = Kons (X -> Bool) which would, by definition, satisfy your requirement, and allow weird functions like f :: X -> Bool defined as f x = case x of Kons g -> g x. Indeed, abusing recursive types like yours, you can write a fixed point combinator and write a non terminating program -- all of that without using explicit term-level recursion. $\endgroup$ – chi Nov 30 '18 at 17:08
  • $\begingroup$ The fact that we can play with such types in functional PLs can help to gain some intuition about how these beasts behave in practice. That, however, tells little about the mathematical side, i.e. about models of the PL at hand. For that, one needs to dive into domain theory, as Andrej Bauer points out below, to get a satisfactory understanding. A bit of category theory (F-algebras and colimits) would also help to construct these domains. $\endgroup$ – chi Nov 30 '18 at 17:11
5
$\begingroup$

To say that we cannot solve $X \cong (X \to 2)$ in sets means that we have to do it in another category. And because we're talking programming languages, we should be looking for one in domain theory. The buzzword to look for is recursive domain equation.

There are several kinds of domains, but to give you an idea of what they are, perhaps we can recall the definition of $\omega$-cpos. An $\omega$-cpo $(P, {\leq})$ is a set $P$ with a partial order $\leq$ which has a least element $\bot \in P$ and such that every increasing sequence $x_0 \leq x_1 \leq x_2 \leq \cdots$ in $P$ has a supremum.

In the particular case we look for a domain $X$ which satisfies $$X \cong [X \to 2_\bot]$$ where:

  • the domain $2_\bot = \{0, 1, \bot\}$ is ordered by $\bot \leq 0$, $\bot \leq 1$ (i.e., $\bot$ is below $0$ and $1$, and $0$ and $1$ are incomparable). The domain $2_\bot$ corresponds to the datatype bool: $0$ and $1$ are the boolean values, while $\bot$ represents a non-terminating program.

  • the domain $[E \to D]$ is the domain all all continuous maps from $E$ to $D$, where a map is said to be continuous if it is monotone and it preserves suprema of increasing chains.

Now, the reason why an equation such as $X \cong [X \to 2_\bot]$ has a solution is complicated. Figuring out that soultions exist when we take a good enough notion of "domain" was done in the early 1970s, with poineering work of Dana Scott and several other people. It takes a short course on domain theory to get to the point where the construction of solutions becomes explainable.

Perhaps I can comment on why domain theory avoids the usual problem from set theory, where Cantor's diagonal argument shows that $X$ always has fewer elements than $X \to 2$. In domain theory $[X \to 2_\bot]$ is not the set of all maps, but just the continuous ones, and there are many fewer of those.

Let's attempt a more familiar setup. Consider the real number $\mathbb{R}$ and the Sierpinski space $\mathbb{S}$, which just the set $2 = \{0, 1\}$ with the topology in which the open sets are $\emptyset$, $\{1\}$ and $\{0, 1\}$. It is well known that the set of continuous maps $\mathcal{C}(\mathbb{R}, \mathbb{S})$ is in bijective correspondence with the open subsets of~$\mathbb{R}$, of which there are $2^{\aleph_0}$, and so we have "solved" $X = X \to 2$ in sets by restricting to continuous maps: $$\mathbb{R} \cong 2^{\aleph_0} \cong \mathcal{C}(\mathbb{R}, \mathbb{S}).$$ This is not a solution, however, because the bijection between $\mathbb{R}$ and $\mathcal{C}(\mathbb{R}, \mathbb{S})$ can never be a homeomorphism.

Sometimes we can actully solve a recursive equation with much less work. For instance, working in topological spaces, we have $$\mathbb{N} \cong 2^{2^\mathbb{N}}$$ because $2^{\mathbb{N}}$ is the Cantor space, whose set of clopen sets is countable and discrete (under the compact-open topology), therefore homeomorphic to $\mathbb{N}$.

Yet another example comes from ordinal arithmetic (not cardinal arithmetic!) where have $2^\omega = \omega$, so that is maybe the closest to what you're asking for.

$\endgroup$

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.