Distinction between a “strictly typed function” and a “not strictly typed function”?
$begingroup$
Let $f$ be the identity function for the real numbers.
In the vernacular, we'd say that $f$ is a function from reals to reals, or that $f:mathbb{R}to mathbb{R}$.
Let $g$ be the inclusion map from the reals to the complex numbers. In the vernacular, we'd say that $g$ maps the reals to the complex numbers.
Now, in certain cases, as far as I can tell, it is useful to say that $f = g$. In fact, in set theory, they'd be the same object. However, in others, it is useful to consider $f$ and $g$ different objects -- after all, $f:mathrm{Real}to mathrm{Real}$, and $g:mathrm{Real}to mathrm{Complex}$ (which occurs a lot in programming languages with a richer typing system).
I'm not trying to argue which is better here, but is there a name for the distinction between these two different treatments of functions?
functions category-theory type-theory
asked Jan 22 at 18:54
extremeaxe5extremeaxe5
577210
$endgroup$
|
show 1 more comment
$begingroup$
Let $f$ be the identity function for the real numbers.
In the vernacular, we'd say that $f$ is a function from reals to reals, or that $f:mathbb{R}to mathbb{R}$.
Let $g$ be the inclusion map from the reals to the complex numbers. In the vernacular, we'd say that $g$ maps the reals to the complex numbers.
Now, in certain cases, as far as I can tell, it is useful to say that $f = g$. In fact, in set theory, they'd be the same object. However, in others, it is useful to consider $f$ and $g$ different objects -- after all, $f:mathrm{Real}to mathrm{Real}$, and $g:mathrm{Real}to mathrm{Complex}$ (which occurs a lot in programming languages with a richer typing system).
I'm not trying to argue which is better here, but is there a name for the distinction between these two different treatments of functions?
functions category-theory type-theory
asked Jan 22 at 18:54
extremeaxe5extremeaxe5
577210
$endgroup$
1
$begingroup$
Pedantically, since $mathbb{C} = mathbb{R}^2$, those two maps would not be the same in $textbf{Set}$ (unless you compose $g$ with $pi_1$).
$endgroup$
– Metric
Jan 23 at 3:19
$begingroup$
@Metric Really? I'm pretty sure the standard definition of $mathbb{C}$ is $mathbb{R}'^2$, and then $mathbb{R}$ is defined as a subfield of $mathbb{C}$ -- basically, yes, you first have to define something like $mathbb{R}$, but then you hack it so that $mathbb{R}subseteq mathbb{C}$.
$endgroup$
– extremeaxe5
Jan 24 at 1:27
$begingroup$
Yes, really. No, it's $mathbb{C} = mathbb{R}^2$.
$endgroup$
– Metric
Jan 24 at 23:43
$begingroup$
@Metric us.metamath.org/mpeuni/mmcomplex.html#axioms "We later define natural numbers, integers, and rational numbers as specific subsets of ℂ, leading to the nice relationships ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ."
$endgroup$
– extremeaxe5
Jan 24 at 23:58
$begingroup$
Which is not standard.
$endgroup$
– Metric
Jan 25 at 0:05
|
show 1 more comment
$begingroup$
Let $f$ be the identity function for the real numbers.
In the vernacular, we'd say that $f$ is a function from reals to reals, or that $f:mathbb{R}to mathbb{R}$.
Let $g$ be the inclusion map from the reals to the complex numbers. In the vernacular, we'd say that $g$ maps the reals to the complex numbers.
Now, in certain cases, as far as I can tell, it is useful to say that $f = g$. In fact, in set theory, they'd be the same object. However, in others, it is useful to consider $f$ and $g$ different objects -- after all, $f:mathrm{Real}to mathrm{Real}$, and $g:mathrm{Real}to mathrm{Complex}$ (which occurs a lot in programming languages with a richer typing system).
I'm not trying to argue which is better here, but is there a name for the distinction between these two different treatments of functions?
functions category-theory type-theory
asked Jan 22 at 18:54
extremeaxe5extremeaxe5
577210
$endgroup$
Let $f$ be the identity function for the real numbers.
In the vernacular, we'd say that $f$ is a function from reals to reals, or that $f:mathbb{R}to mathbb{R}$.
Let $g$ be the inclusion map from the reals to the complex numbers. In the vernacular, we'd say that $g$ maps the reals to the complex numbers.
Now, in certain cases, as far as I can tell, it is useful to say that $f = g$. In fact, in set theory, they'd be the same object. However, in others, it is useful to consider $f$ and $g$ different objects -- after all, $f:mathrm{Real}to mathrm{Real}$, and $g:mathrm{Real}to mathrm{Complex}$ (which occurs a lot in programming languages with a richer typing system).
I'm not trying to argue which is better here, but is there a name for the distinction between these two different treatments of functions?
functions category-theory type-theory
functions category-theory type-theory
asked Jan 22 at 18:54
extremeaxe5extremeaxe5
577210
asked Jan 22 at 18:54
extremeaxe5extremeaxe5
577210
asked Jan 22 at 18:54
extremeaxe5extremeaxe5
577210
asked Jan 22 at 18:54
extremeaxe5extremeaxe5
577210
asked Jan 22 at 18:54
extremeaxe5extremeaxe5
577210
577210
1
$begingroup$
Pedantically, since $mathbb{C} = mathbb{R}^2$, those two maps would not be the same in $textbf{Set}$ (unless you compose $g$ with $pi_1$).
$endgroup$
– Metric
Jan 23 at 3:19
$begingroup$
@Metric Really? I'm pretty sure the standard definition of $mathbb{C}$ is $mathbb{R}'^2$, and then $mathbb{R}$ is defined as a subfield of $mathbb{C}$ -- basically, yes, you first have to define something like $mathbb{R}$, but then you hack it so that $mathbb{R}subseteq mathbb{C}$.
$endgroup$
– extremeaxe5
Jan 24 at 1:27
$begingroup$
Yes, really. No, it's $mathbb{C} = mathbb{R}^2$.
$endgroup$
– Metric
Jan 24 at 23:43
$begingroup$
@Metric us.metamath.org/mpeuni/mmcomplex.html#axioms "We later define natural numbers, integers, and rational numbers as specific subsets of ℂ, leading to the nice relationships ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ."
$endgroup$
– extremeaxe5
Jan 24 at 23:58
$begingroup$
Which is not standard.
$endgroup$
– Metric
Jan 25 at 0:05
|
show 1 more comment
1
$begingroup$
Pedantically, since $mathbb{C} = mathbb{R}^2$, those two maps would not be the same in $textbf{Set}$ (unless you compose $g$ with $pi_1$).
$endgroup$
– Metric
Jan 23 at 3:19
$begingroup$
@Metric Really? I'm pretty sure the standard definition of $mathbb{C}$ is $mathbb{R}'^2$, and then $mathbb{R}$ is defined as a subfield of $mathbb{C}$ -- basically, yes, you first have to define something like $mathbb{R}$, but then you hack it so that $mathbb{R}subseteq mathbb{C}$.
$endgroup$
– extremeaxe5
Jan 24 at 1:27
$begingroup$
Yes, really. No, it's $mathbb{C} = mathbb{R}^2$.
$endgroup$
– Metric
Jan 24 at 23:43
$begingroup$
@Metric us.metamath.org/mpeuni/mmcomplex.html#axioms "We later define natural numbers, integers, and rational numbers as specific subsets of ℂ, leading to the nice relationships ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ."
$endgroup$
– extremeaxe5
Jan 24 at 23:58
$begingroup$
Which is not standard.
$endgroup$
– Metric
Jan 25 at 0:05
1
1
$begingroup$
Pedantically, since $mathbb{C} = mathbb{R}^2$, those two maps would not be the same in $textbf{Set}$ (unless you compose $g$ with $pi_1$).
$endgroup$
– Metric
Jan 23 at 3:19
$begingroup$
Pedantically, since $mathbb{C} = mathbb{R}^2$, those two maps would not be the same in $textbf{Set}$ (unless you compose $g$ with $pi_1$).
$endgroup$
– Metric
Jan 23 at 3:19
$begingroup$
@Metric Really? I'm pretty sure the standard definition of $mathbb{C}$ is $mathbb{R}'^2$, and then $mathbb{R}$ is defined as a subfield of $mathbb{C}$ -- basically, yes, you first have to define something like $mathbb{R}$, but then you hack it so that $mathbb{R}subseteq mathbb{C}$.
$endgroup$
– extremeaxe5
Jan 24 at 1:27
$begingroup$
@Metric Really? I'm pretty sure the standard definition of $mathbb{C}$ is $mathbb{R}'^2$, and then $mathbb{R}$ is defined as a subfield of $mathbb{C}$ -- basically, yes, you first have to define something like $mathbb{R}$, but then you hack it so that $mathbb{R}subseteq mathbb{C}$.
$endgroup$
– extremeaxe5
Jan 24 at 1:27
$begingroup$
Yes, really. No, it's $mathbb{C} = mathbb{R}^2$.
$endgroup$
– Metric
Jan 24 at 23:43
$begingroup$
Yes, really. No, it's $mathbb{C} = mathbb{R}^2$.
$endgroup$
– Metric
Jan 24 at 23:43
$begingroup$
@Metric us.metamath.org/mpeuni/mmcomplex.html#axioms "We later define natural numbers, integers, and rational numbers as specific subsets of ℂ, leading to the nice relationships ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ."
$endgroup$
– extremeaxe5
Jan 24 at 23:58
$begingroup$
@Metric us.metamath.org/mpeuni/mmcomplex.html#axioms "We later define natural numbers, integers, and rational numbers as specific subsets of ℂ, leading to the nice relationships ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ."
$endgroup$
– extremeaxe5
Jan 24 at 23:58
$begingroup$
Which is not standard.
$endgroup$
– Metric
Jan 25 at 0:05
$begingroup$
Which is not standard.
$endgroup$
– Metric
Jan 25 at 0:05
|
show 1 more comment
0
active
oldest
votes
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%2f3083550%2fdistinction-between-a-strictly-typed-function-and-a-not-strictly-typed-functi%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
0
active
oldest
votes
0
active
oldest
votes
active
oldest
votes
active
oldest
votes
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%2f3083550%2fdistinction-between-a-strictly-typed-function-and-a-not-strictly-typed-functi%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
1
$begingroup$
Pedantically, since $mathbb{C} = mathbb{R}^2$, those two maps would not be the same in $textbf{Set}$ (unless you compose $g$ with $pi_1$).
$endgroup$
– Metric
Jan 23 at 3:19
$begingroup$
@Metric Really? I'm pretty sure the standard definition of $mathbb{C}$ is $mathbb{R}'^2$, and then $mathbb{R}$ is defined as a subfield of $mathbb{C}$ -- basically, yes, you first have to define something like $mathbb{R}$, but then you hack it so that $mathbb{R}subseteq mathbb{C}$.
$endgroup$
– extremeaxe5
Jan 24 at 1:27
$begingroup$
Yes, really. No, it's $mathbb{C} = mathbb{R}^2$.
$endgroup$
– Metric
Jan 24 at 23:43
$begingroup$
@Metric us.metamath.org/mpeuni/mmcomplex.html#axioms "We later define natural numbers, integers, and rational numbers as specific subsets of ℂ, leading to the nice relationships ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ."
$endgroup$
– extremeaxe5
Jan 24 at 23:58
$begingroup$
Which is not standard.
$endgroup$
– Metric
Jan 25 at 0:05