C-like type declaration.
$begingroup$
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}
$$
soft-question notation type-theory
asked Jan 13 at 14:26
SeninhaSeninha
1265
$endgroup$
add a comment |
$begingroup$
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}
$$
soft-question notation type-theory
asked Jan 13 at 14:26
SeninhaSeninha
1265
$endgroup$
3
$begingroup$
In "most" math books? I have never seen this in 30+ years.
$endgroup$
– Martin Argerami
Jan 13 at 14:28
1
$begingroup$
No, people do not write $n:Bbb N$ to "declare" $n$. They write $ninBbb N$; which is an assertion to the effect that $n$ is an element of $Bbb N$. Yes, people do write $f:Bbb RtoBbb 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.
$endgroup$
– David C. Ullrich
Jan 13 at 14:41
add a comment |
$begingroup$
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}
$$
soft-question notation type-theory
asked Jan 13 at 14:26
SeninhaSeninha
1265
$endgroup$
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}
$$
soft-question notation type-theory
soft-question notation type-theory
asked Jan 13 at 14:26
SeninhaSeninha
1265
asked Jan 13 at 14:26
SeninhaSeninha
1265
edited Jan 13 at 14:30
Seninha
asked Jan 13 at 14:26
SeninhaSeninha
1265
asked Jan 13 at 14:26
SeninhaSeninha
1265
asked Jan 13 at 14:26
SeninhaSeninha
1265
1265
3
$begingroup$
In "most" math books? I have never seen this in 30+ years.
$endgroup$
– Martin Argerami
Jan 13 at 14:28
1
$begingroup$
No, people do not write $n:Bbb N$ to "declare" $n$. They write $ninBbb N$; which is an assertion to the effect that $n$ is an element of $Bbb N$. Yes, people do write $f:Bbb RtoBbb 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.
$endgroup$
– David C. Ullrich
Jan 13 at 14:41
add a comment |
3
$begingroup$
In "most" math books? I have never seen this in 30+ years.
$endgroup$
– Martin Argerami
Jan 13 at 14:28
1
$begingroup$
No, people do not write $n:Bbb N$ to "declare" $n$. They write $ninBbb N$; which is an assertion to the effect that $n$ is an element of $Bbb N$. Yes, people do write $f:Bbb RtoBbb 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.
$endgroup$
– David C. Ullrich
Jan 13 at 14:41
3
3
$begingroup$
In "most" math books? I have never seen this in 30+ years.
$endgroup$
– Martin Argerami
Jan 13 at 14:28
$begingroup$
In "most" math books? I have never seen this in 30+ years.
$endgroup$
– Martin Argerami
Jan 13 at 14:28
1
1
$begingroup$
No, people do not write $n:Bbb N$ to "declare" $n$. They write $ninBbb N$; which is an assertion to the effect that $n$ is an element of $Bbb N$. Yes, people do write $f:Bbb RtoBbb 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.
$endgroup$
– David C. Ullrich
Jan 13 at 14:41
$begingroup$
No, people do not write $n:Bbb N$ to "declare" $n$. They write $ninBbb N$; which is an assertion to the effect that $n$ is an element of $Bbb N$. Yes, people do write $f:Bbb RtoBbb 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.
$endgroup$
– David C. Ullrich
Jan 13 at 14:41
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
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}tomathbb{R}\:xmapsto 2xend{align*}
respectively. No need to mess around with arcane patterns and arrangements of symbols that do nothing but make the text harder to read.
answered Jan 13 at 14:34
user3482749user3482749
4,206919
$endgroup$
$begingroup$
I agree with everything, but the second set of colons in the definition of the function would be highly unusual.
$endgroup$
– Martin Argerami
Jan 13 at 15:26
$begingroup$
@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.
$endgroup$
– user3482749
Jan 13 at 15:28
$begingroup$
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).
$endgroup$
– Giorgio Mossa
Jan 13 at 16:58
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3072047%2fc-like-type-declaration%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
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}tomathbb{R}\:xmapsto 2xend{align*}
respectively. No need to mess around with arcane patterns and arrangements of symbols that do nothing but make the text harder to read.
answered Jan 13 at 14:34
user3482749user3482749
4,206919
$endgroup$
$begingroup$
I agree with everything, but the second set of colons in the definition of the function would be highly unusual.
$endgroup$
– Martin Argerami
Jan 13 at 15:26
$begingroup$
@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.
$endgroup$
– user3482749
Jan 13 at 15:28
$begingroup$
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).
$endgroup$
– Giorgio Mossa
Jan 13 at 16:58
add a comment |
$begingroup$
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}tomathbb{R}\:xmapsto 2xend{align*}
respectively. No need to mess around with arcane patterns and arrangements of symbols that do nothing but make the text harder to read.
answered Jan 13 at 14:34
user3482749user3482749
4,206919
$endgroup$
$begingroup$
I agree with everything, but the second set of colons in the definition of the function would be highly unusual.
$endgroup$
– Martin Argerami
Jan 13 at 15:26
$begingroup$
@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.
$endgroup$
– user3482749
Jan 13 at 15:28
$begingroup$
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).
$endgroup$
– Giorgio Mossa
Jan 13 at 16:58
add a comment |
$begingroup$
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}tomathbb{R}\:xmapsto 2xend{align*}
respectively. No need to mess around with arcane patterns and arrangements of symbols that do nothing but make the text harder to read.
answered Jan 13 at 14:34
user3482749user3482749
4,206919
$endgroup$
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}tomathbb{R}\:xmapsto 2xend{align*}
respectively. No need to mess around with arcane patterns and arrangements of symbols that do nothing but make the text harder to read.
answered Jan 13 at 14:34
user3482749user3482749
4,206919
answered Jan 13 at 14:34
user3482749user3482749
4,206919
answered Jan 13 at 14:34
user3482749user3482749
4,206919
answered Jan 13 at 14:34
user3482749user3482749
4,206919
4,206919
$begingroup$
I agree with everything, but the second set of colons in the definition of the function would be highly unusual.
$endgroup$
– Martin Argerami
Jan 13 at 15:26
$begingroup$
@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.
$endgroup$
– user3482749
Jan 13 at 15:28
$begingroup$
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).
$endgroup$
– Giorgio Mossa
Jan 13 at 16:58
add a comment |
$begingroup$
I agree with everything, but the second set of colons in the definition of the function would be highly unusual.
$endgroup$
– Martin Argerami
Jan 13 at 15:26
$begingroup$
@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.
$endgroup$
– user3482749
Jan 13 at 15:28
$begingroup$
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).
$endgroup$
– Giorgio Mossa
Jan 13 at 16:58
$begingroup$
I agree with everything, but the second set of colons in the definition of the function would be highly unusual.
$endgroup$
– Martin Argerami
Jan 13 at 15:26
$begingroup$
I agree with everything, but the second set of colons in the definition of the function would be highly unusual.
$endgroup$
– Martin Argerami
Jan 13 at 15:26
$begingroup$
@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.
$endgroup$
– user3482749
Jan 13 at 15:28
$begingroup$
@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.
$endgroup$
– user3482749
Jan 13 at 15:28
$begingroup$
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).
$endgroup$
– Giorgio Mossa
Jan 13 at 16:58
$begingroup$
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).
$endgroup$
– Giorgio Mossa
Jan 13 at 16:58
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3072047%2fc-like-type-declaration%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
3
$begingroup$
In "most" math books? I have never seen this in 30+ years.
$endgroup$
– Martin Argerami
Jan 13 at 14:28
1
$begingroup$
No, people do not write $n:Bbb N$ to "declare" $n$. They write $ninBbb N$; which is an assertion to the effect that $n$ is an element of $Bbb N$. Yes, people do write $f:Bbb RtoBbb 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.
$endgroup$
– David C. Ullrich
Jan 13 at 14:41