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?
floor(x)
andsgn(x)
are provided by all programming languages and they are not continuous. $\endgroup$floor
andsgn
are computable because their domain is floating-point numbers. On all reals, they are not computable. $\endgroup$