Do "seemingly impossible functional programs" work with arrow types interpreted as Turing machines?

$\newcommand{\E}[1]{\mathtt{E}_{#1}}$

You are indeed using the model of computability that corresponds to the effective topos. It is also called hereditarily effective operators (HEO), Type I computability, and Russian constructivism. These things got invented several times.

Let us first recall a couple of definitions, and generally set things up in a reasonable way so that we do not have to fiddle with Turing machines. We work constructively, so that everything we say works in the effective topos, as well as in many other toposes (such as classical set theory).

For the purposes of this answer, say that a set $X$ is searchable if there exists a map $\E{X} : 2^X \to 2$, where $2 = \{0,1\}$ is the discrete two-point set, such that for all predicates $p : X \to 2$ $$\E{X}(p) = 1 \iff \exists x \in X \,.\, p(x) = 1.$$ We would like to know whether the Cantor space $\mathsf{C} = 2^\mathbb{N}$ is searchable in the effective topos.

We do not know how to directly construct the map $\E{\mathsf{C}}$, but we do know how to write it down as a relation, i.e., define $F \subseteq 2^\mathsf{C} \times 2$ by $$F(p, b) \iff ((\exists \alpha \in \mathsf{C} \,.\, p(\alpha) = 1) \iff b = 1).$$ This is a single-valued relation: for every $p \in 2^\mathsf{C}$ there is at most one $b \in 2$ such that $F(p, b)$. Therefore, a priori $F$ yields a partial map $E : 2^\mathsf{C} \rightharpoonup 2$, defined by, $$E(p) = b \iff F(p, b),$$ with the domain of definition $$D = \{ p \in 2^\mathsf{C} \mid \exists b \in 2 \,.\, F(p, b) \}.$$ The map $E$ is our candidate for $\E{\mathsf{C}}$, but we do not know whether its domain of definition $D$ is all of $2^\mathsf{C}$.

Recall that the Cantor space is a complete separable metric space, with the (ultra)metric defined by $$d(\alpha, \beta) = \lim_{k \to \infty} 2^{- \min \{i \leq k \mid i = k \lor \alpha_i \neq \beta_i\}}$$ The formula is written this way so that it works constructively (and therefore computably). We have $d(\alpha, \beta) = 2^{-i}$ if $i$ is the least index for which $\alpha_i \neq \beta_i$.

The domain $D$ is not small:

Proposition 1: $D$ contains the uniformly continuous predicates.

Proof. A uniformly continuous predicate $p : \mathsf{C} \to 2$ has a nice tree representation from which it is easy to calculate whether $p$ attains $1$. $\Box$

Proposition 1 explains that the Cantor space is searchable in toposes that validate the statement "every map $\mathsf{C} \to 2$ is uniformly continuous" (because then $2^\mathsf{C} \subseteq D \subseteq 2^\mathsf{C}$). An example is the Kleene-Vesley topos, also known as Type II computability and Brouwerian intuitionism.

However, in the effective topos things are strange. Recall that the Baire space $\mathsf{B} = \mathbb{N}^\mathbb{N}$ is also a complete separable metric space, with the metric defined by the same formula above as for the Cantor space. Many questions about Cantor space in the effective topos may be answered using the following theorem.

Theorem 2 (effective topos): The Cantor space and the Baire space are homeomorphic as complete metric spaces.

The proof relies on the existence of a Kleene tree. This is a strange theorem indeed, since classically the Cantor space is compact and the Baire space is locally non-compact (every open ball contains a sequence without an accumulation point).

Proposition 3: If $X$ is searchable and there is a surjection $s : X \to Y$ then $Y$ is searchable.

Proof. $\E{Y}(p) = \E{X}(p \circ s)$. $\Box$

Proposition 4: If $\mathbb{N}$ is searchable then LPO holds.

Proof. Exercise $\Box$.

Theorem 5 (effective topos): The Cantor space is not searchable.

Proof. Suppose we had $D = 2^\mathsf{C}$, so that $\mathsf{C}$ is searchable with $\E{\mathsf{C}} = E$. By Theorem 2 there is a surjection $\mathsf{C} \to \mathsf{B}$, therefore $\mathsf{B}$ is searchable. There is also a surjection $\mathsf{B} \to \mathbb{N}$, namely $\alpha \mapsto \alpha(0)$, hence $\mathbb{N}$ is searchable. By Proposition 4 LPO holds. But LPO is invalid in the effective topos, because it implies the existence of a Halting oracle. $\Box$

And lastly, let us explain why it is so easy to get confused about searchability of Cantor space. While we proved that in the effective topos $D$ is a proper subset of $2^\mathsf{C}$, the complement $2^\mathsf{C} \setminus D$ is always empty!

Proposition 6: $2^\mathsf{C} \setminus D = \emptyset$.

Proof. Notice that $$D = \{ p \in 2^\mathsf{C} \mid (\exists \alpha \in \mathsf{C} \,.\, p(\alpha) = 1) \lor (\forall \alpha \in \mathsf{C}\,.\, p(\alpha) = 0)\}.$$ Suppose we had $q \in 2^\mathsf{C} \setminus D$. Then it follows that $$\lnot ((\exists \alpha \in \mathsf{C} \,.\, q(\alpha) = 1) \lor (\forall \alpha \in \mathsf{C}\,.\, q(\alpha) = 0))$$ which is equivalent to $$(\forall \alpha \in \mathsf{C} \,.\, q(\alpha) = 0) \land \lnot (\forall \alpha \in \mathsf{C}\,.\, q(\alpha) = 0)$$ which is false. $\Box$

The conclusion is strange but not contradictory: we can never produce a concrete predicate $p \in 2^\mathsf{C}$ for which $E$ does not work, while on the other hand in the effective topos $E$ does not work correctly on all of $2^\mathsf{C}$. Translated to classical computability, the same conclusion is perhaps a little bit easier to swallow: every computable predicate on the computable Cantor space either attains $1$ or it does not, but there is no computable procedure for determining whether computable predicates on Cantor space attain $1$.