What is the "continuity" as a term in computable analysis?

Background

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

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?

Different people have different views on what the definition of continuity should be, but the way I see it, we should define continuity to be computability relative to some oracle. For example:

Definition: A function $f : \mathbf{X} \to \mathbf{Y}$ is continuous, if there is a computable partial function $F :\subseteq \mathbf{X} \times \mathbb{N}^\mathbb{N} \to \mathbf{Y}$ and some $p \in \mathbb{N}^\mathbb{N}$ such that $f(x) = F(x,p)$.

So the most primitive concept in handling a space is what representation we are using for it, which then yields the notion of computability, and from that we get the notion of continuity.

So far, the definition of continuity seems rather unrelated to continuity from topology, and one may wonder why that term has been chosen. One reason is that we usually use admissible representations, which have the characterization that the functions between them which are continuous in the computable analysis definition are exactly the functions which are continuous in the topological sense.

If we have an admissible representation $\delta : \subseteq \Sigma^\mathbb{N} \to \mathbf{X}$, we get the topology on $\mathbf{X}$ as the final topology along $\delta$, i.e. a set $U \subseteq \mathbf{X}$ is open iff there is a set $W$ of finite words such that $\delta^{-1}(U) = \operatorname{dom}(\delta) \cap \bigcup_{w \in W} w\Sigma^\mathbb{N}$. Matthias Schröder has shown that the topological spaces which have admissible representations are exactly the $T_0$ quotients of countably-based spaces.

Now to slowly come back to the starting point of your question, what prevents us from using the discrete topology on the reals? The reason we cannot do that is that every countably-based space is separable, ie has a (countable) dense sequence. Taking quotients preserves being separable, so every topology associated to a representation is necessarily separable. A discrete space is separable iff it is countable, so we cannot get the discrete topology on the reals.

There is a way to get an admissible representation of $\mathbb{R}$ that makes $\mathbb{Q}$ a discrete subspace (essentially, treat $\mathbb{R}$ as $\mathbb{N}^{*} \cup \mathbb{N}^\mathbb{N}$), but as you have argued in the question, that makes addition uncomputable (and overall, has very little resemblance to the reals as we would want them).

On a side note, that we cannot avoid getting stuck without even recognising it when accidentally trying to divide by $0$ is a significant obstacle if we are trying to do linear algebra with real numbers.

References:

Pieter Collins:
Computable analysis with applications to dynamic systems. Math. Struct. Comput. Sci. 30(2): 173-233 (2020)

Martín Hötzel Escardó:
Synthetic Topology: of Data Types and Classical Spaces. Electron. Notes Theor. Comput. Sci. 87: 21-156 (2004)

Takayuki Kihara, Arno Pauly: Dividing by Zero - How Bad Is It, Really?. MFCS 2016: 58:1-58:14

Arno Pauly: On the topological aspects of the theory of represented spaces. Computability 5(2): 159-180 (2016) arXiv

Matthias Schröder:
Extended admissibility. Theor. Comput. Sci. 284(2): 519-538 (2002)

StackExchange Computer Science Q#129490, answer score: 8