What is the role of impredicativity in program extraction?

Question

Is impredicativity useful for program extraction in Coq? For example is there some kind of realizability argument that depends on impredicativity?

Of course it doesn't seem to be necessary for program extraction, as Agda manages to extract programs to Haskell, but I suspect there might be some kind of theoretical tradeoff.

Answer 1

I have occasionally thought about this question. My inconclusive conclusion is that impredicativity hinders program extraction. Let me try to give an argument in the context of realizability. I am going to crank up the technical level of the discussion, because the concepts involved are, well, a bit technical (but they also embody some pretty concrete intuitions).

Assume we're working in a realizability topos over a pca $\mathbb{A}$. Now, that's a pretty big and complicated category, which among other things contains $\mathsf{Set}$ as a full subcategory: given any set $X$, we get an object $\nabla X = (X, {\Vdash_{\nabla X}})$ in the topos whose realizability relation is trivial: $r \Vdash_{\nabla X} x$ holds for all $r \in \mathbb{A}$ and all $x \in X$. From a computational point of view the realizers of $\nabla X$ are maximally uninformative because every realizer $r$ realizes every element of $X$.

So if the realizability topos can contain such computationally trivial objects, perhaps we should try to define precisely what it means for an object to be computationally trivial in general.

Here is a bad attempt: say that an object $S$ of the topos is computationally trivial if every morphism $S \to \mathsf{Bool}$ is constant, where $\mathsf{Bool} = 1 + 1$ is the object of Booleans. The idea is right, namely $S$ should be considered computationally trivial if we can't extract any interesting bits of information from it, but the execution is wrong, because sometimes we can extract less than one bit. (For instance, we can't decide whether any given machine halts, but we can semi-decide that it halts.)

Given any disjoint non-empty subsets $T_0, T_1 \subseteq \mathbb{A}$ define the test object $[T_0, T_1]$ to be the set $\{0,1\}$ with the realizability relation $$r \Vdash_{[T_0, T_1]} b \iff (r \in T_1 \land b = 1) \lor (r \in T_0 \land b = 0). $$ In words, $1$ is realized by the elements of $T_1$ and $0$ by the elements of $T_0$. Examples:

• Decidable test: $T_0 = \{\mathtt{false}\}$ and $T_1 = \{\mathtt{true}\}$ yields the booleans,
• Semi-decidable test: $T_0 = \{\ulcorner M \urcorner \mid \text{machine $M$ does not halt on input $\ulcorner M \urcorner$}\}$ and $T_1 = \{\ulcorner M \urcorner \mid \text{machine $M$ halts on input $\ulcorner M \urcorner$}\}$.
• We can make much weaker notions of test than decidability and semi-decidability. Write $\mathsf{PA} \models \phi$ if the sentence $\phi$ in the language of Peano arithmetic is true, and define $$T_0 = \{ \ulcorner \phi \urcorner \mid \mathsf{PA} \models \phi\}$$ and $$T_1 = \{ \ulcorner \phi \urcorner \mid \mathsf{PA} \models \lnot\phi \}.$$ This sort of test is very weak. It is not about deciding arithmetical sentences, but rather expresing conditions with arithmetical formulas. Indeed, suppose $r \Vdash_{[T_0, T_1]} b$. Then $r$ encodes some arithmetical sentence $\phi$ such that $b = 1 \Leftrightarrow \mathsf{PA} \models \phi$ – so telling which bit $r$ encodes is as hard as computing arithmetical truth.

A morphism $f : S \to [T_0, T_1]$ can be thought of as a two-valued test.

Definition: An object $S$ of the realizability topos is computationally trivial if for all test objects $[T_0, T_1]$ all morphisms $S \to [T_0, T_1]$ are constant.

What the definition says is that one cannot extract any non-trivial information from $S$, for any notion of two-valued test.

Proposition: For any set $X$, the object $\nabla X$ is computationally trivial.

Here is the punchline: impredicativity is intimately tied to completeness, bu completeness prevents extraction of any useful information.

Theorem: A complete lattice is computationally trivial.

Proof. We already know that $\nabla \{0,1\}$ is computationally trivial. Now consider any complete lattice $L$, a test object $[T_0, T_1]$ and a morphism $f : L \to [T_0, T_1]$. Given $x \in L$, define $g : \nabla \{0,1\} \to L$ by $$g(p) = \sup \{ y \in L \mid y = x \land p = 1 \}$$ The map $f \circ g : \nabla \{0,1\} \to [T_0, T_1]$ is constant, therefore $$f(\bot) = f(g(0)) = f(g(1)) = f(x),$$ which shows that $f$ is constant. $\Box$

P.S. A comment for the connoisseurs: all the above says is that all morphisms from a complete lattice to a modest set are constant.