What is the “continuity” as a term in computable analysis?


I once implemented a datatype representing arbitrary real numbers in Haskell. It labels every real numbers by having a Cauchy sequence converging to it. That will let $ \mathbb{R}$ be in the usual topology. I also implemented addition, subtraction, multiplication, and division.

But my teacher said, "This doesn’t seem to be a good idea. Since comparison is undecidable here, this doesn’t look very practical. In particular, letting division by 0 to fall in an infinite loop doesn’t look good."

So I wanted my datatype to extend $ \mathbb{Q}$ . Since equality comparison of $ \mathbb{Q}$ is decidable, $ \mathbb{Q}$ is in discrete topology. That means a topology on $ \mathbb{R}$ must be finer than the discrete topology on $ \mathbb{Q}$ .

But, I think I found that, even if I could implement such datatype, it will be impractical.

Proof, step 1

Let $ \mathbb{R}$ be finer than $ \mathbb{Q}$ in discrete topology. Then $ \{0\}$ is open in $ \mathbb{R}$ . Assume $ + : \mathbb{R}^2 → \mathbb{R}$ is continuous. Then $ \{(x,-x): x \in \mathbb{R}\}$ is open in $ \mathbb{R}^2$ . Since $ \mathbb{R}^2$ is in product topology, $ \{(x,-x)\}$ is a basis element of $ \mathbb{R}^2$ for every $ x \in \mathbb{R}$ . It follows that $ \{x\}$ is a basis element of $ \mathbb{R}$ for every $ x \in \mathbb{R}$ . That is, $ \mathbb{R}$ is in discrete topology.

Proof, step 2

Since $ \mathbb{R}$ is in discrete topology, $ \mathbb{R}$ is computably equality comparable. This is a contradiction, so $ +$ is not continuous, and thus not computable.


What is bugging me is the bolded text. It is well-known that every computable function is continuous (Weihrauch 2000, p. 6). Though the analytic definition and the topological definition of continuity coincide in functions from and to Euclidean spaces, $ \mathbb{R}$ above is not a Euclidean space. So I’m unsure whether my proof is correct. What is the definition of "continuity" in computable analysis?