# C-like type declaration.

In most math books declaring an object along with its type is done with the type after a colon after the object, and the definition of this object is done in another expression. E.g.

\begin{align} n & : \mathbb{N} \\ f & :\mathbb{R} \to \mathbb{R}\\ \\ n & := 3. \\ f & := x \mapsto 2x. \end{align}

When I define an object while declaring its type, I do either the following (with the type of the object in the end, after the definiens):

\begin{align} n & := 3 & : \mathbb{N}. \\ f & := x \mapsto 2x & : \mathbb{R} \to \mathbb{R}. \end{align}

Or the following (with the type of the object after the definiendum):

\begin{align} n & : \mathbb{N} & := 3. \\ f &: \mathbb{R} \to \mathbb{R} & := x \mapsto 2x. \end{align}

But is it right to use a notation like in the C programming language, where the type is written before the object with no colon (like in the following example)? Is there a math book which uses this notation instead of the colon one?

\begin{align} \mathbb{N} & \space n := 3. \\ \mathbb{R} \to \mathbb{R} & \space f := x \mapsto 2x. \end{align}

• In "most" math books? I have never seen this in 30+ years. Jan 13 '19 at 14:28
• No, people do not write $n:\Bbb N$ to "declare" $n$. They write $n\in\Bbb N$; which is an assertion to the effect that $n$ is an element of $\Bbb N$. Yes, people do write $f:\Bbb R\to\Bbb R$, but I think it's misleading to think of the colon there as a "declaration" - in fact that line says $f$ is a function from $\Bbb R$ to itself. Jan 13 '19 at 14:41

## 1 Answer

All four of these are horrible to read. The closest that I've seen to your last is $$f: \mathbb{R}\ni x \mapsto 2x \in \mathbb{R}$$, but that's rare and hiddeous as well. We aren't doing programming: what we're writing is intended to be readable by humans, not parseable by computers. Therefore, you should write something that is easy for humans to read. Sentences are easy for humans to read. For your examples, I'd write "let $$x = 3$$" (no need to specify that it's natural: we can see that) and Define \begin{align*}f:\mathbb{R}\to\mathbb{R}\\:x\mapsto 2x\end{align*}

respectively. No need to mess around with arcane patterns and arrangements of symbols that do nothing but make the text harder to read.

• I agree with everything, but the second set of colons in the definition of the function would be highly unusual. Jan 13 '19 at 15:26
• @MartinArgerami True. I was going for something relatively close to what was in the question, but actually understandable by mathematicians. I figured including the colon at least isn't confusing to anybody. Leaving it out is definitely more common. Jan 13 '19 at 15:28
• Also, if I may add, a lot of new programming languages are using a more math-like typing discipline (for instance Go and Rust, just to cite some non functional languages). Jan 13 '19 at 16:58