Mixing
Can we see categories as programming languages?
$begingroup$
In this video, category theory is explained to an audience of programmers. The speaker says that we can think of a category as a programming language, and of objects as types in that language, and morphisms as static methods from type to type.
To what extent is this perspective correct? Are there major issues with it?
ps. How does this relate to the curry howard lambek isomorphism?
category-theory lambda-calculus
asked Jan 27 at 9:34
user56834user56834
3,49421253
$endgroup$
add a comment |
$begingroup$
In this video, category theory is explained to an audience of programmers. The speaker says that we can think of a category as a programming language, and of objects as types in that language, and morphisms as static methods from type to type.
To what extent is this perspective correct? Are there major issues with it?
ps. How does this relate to the curry howard lambek isomorphism?
category-theory lambda-calculus
asked Jan 27 at 9:34
user56834user56834
3,49421253
$endgroup$
1
$begingroup$
Functional programming goes in this direction.
$endgroup$
– Wuestenfux
Jan 27 at 9:35
$begingroup$
You could also explain category theory to a person having only a hammer by saying that objects are nails ...
$endgroup$
– Hagen von Eitzen
Jan 27 at 9:38
add a comment |
$begingroup$
In this video, category theory is explained to an audience of programmers. The speaker says that we can think of a category as a programming language, and of objects as types in that language, and morphisms as static methods from type to type.
To what extent is this perspective correct? Are there major issues with it?
ps. How does this relate to the curry howard lambek isomorphism?
category-theory lambda-calculus
asked Jan 27 at 9:34
user56834user56834
3,49421253
$endgroup$
In this video, category theory is explained to an audience of programmers. The speaker says that we can think of a category as a programming language, and of objects as types in that language, and morphisms as static methods from type to type.
To what extent is this perspective correct? Are there major issues with it?
ps. How does this relate to the curry howard lambek isomorphism?
category-theory lambda-calculus
category-theory lambda-calculus
asked Jan 27 at 9:34
user56834user56834
3,49421253
asked Jan 27 at 9:34
user56834user56834
3,49421253
asked Jan 27 at 9:34
user56834user56834
3,49421253
asked Jan 27 at 9:34
user56834user56834
3,49421253
asked Jan 27 at 9:34
user56834user56834
3,49421253
3,49421253
1
$begingroup$
Functional programming goes in this direction.
$endgroup$
– Wuestenfux
Jan 27 at 9:35
$begingroup$
You could also explain category theory to a person having only a hammer by saying that objects are nails ...
$endgroup$
– Hagen von Eitzen
Jan 27 at 9:38
add a comment |
1
$begingroup$
Functional programming goes in this direction.
$endgroup$
– Wuestenfux
Jan 27 at 9:35
$begingroup$
You could also explain category theory to a person having only a hammer by saying that objects are nails ...
$endgroup$
– Hagen von Eitzen
Jan 27 at 9:38
1
1
$begingroup$
Functional programming goes in this direction.
$endgroup$
– Wuestenfux
Jan 27 at 9:35
$begingroup$
Functional programming goes in this direction.
$endgroup$
– Wuestenfux
Jan 27 at 9:35
$begingroup$
You could also explain category theory to a person having only a hammer by saying that objects are nails ...
$endgroup$
– Hagen von Eitzen
Jan 27 at 9:38
$begingroup$
You could also explain category theory to a person having only a hammer by saying that objects are nails ...
$endgroup$
– Hagen von Eitzen
Jan 27 at 9:38
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
It would make more sense to say that categories are the semantic domains for denotational semantics for type theories (or rather, serve that function rather well). In other words, it would make more sense to say that if you were trying to understand the meaning of a program, you could interpret it into objects and arrows of a category with suitable structure, and then analyze the result mathematically. That said, you can formulate syntactic categories that, as the name suggests, are closer to "programming languages". Really, the best fit would be a presentation of a category (with suitable structure). We can talk about, e.g. the free cartesian closed category generated from a graph.
When we want to talk about cartesian closed categories in general, we typically work with some presentation of them. Usually this happens by asserting that not only do certain universal constructions, e.g. binary products, exist, but that they are chosen by which we mean we have a (bi)functor that actually picks out a specific object to be the binary product of two other objects. This chosen structure, particularly combined with a presentation for the underlying category, provides an abstract, syntactical way of referring to structure within an arbitrary cartesian closed category. It is possible to compile the simply typed lambda calculus (STLC) in terms of this structure in such a way as to validate the reduction rules of the STLC. We can go further and show that all that structure is expressible in terms of the syntax of the STLC in such a way as to validate the universal properties. Altogether this leads to the simply typed lambda calculus being the internal language of cartesian closed categories. This is indeed part of the Curry-Howard-Lambek correspondence.
I haven't watched the video you reference, but there's definitely a way it can be understood to be roughly true. Erik Meijer does know what he's talking about to a reasonable degree with regards to these topics. However, he's often talking to an audience where there's not much value in being very precise.
answered Jan 27 at 11:05
Derek ElkinsDerek Elkins
17.3k11437
$endgroup$
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%2f3089336%2fcan-we-see-categories-as-programming-languages%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$
It would make more sense to say that categories are the semantic domains for denotational semantics for type theories (or rather, serve that function rather well). In other words, it would make more sense to say that if you were trying to understand the meaning of a program, you could interpret it into objects and arrows of a category with suitable structure, and then analyze the result mathematically. That said, you can formulate syntactic categories that, as the name suggests, are closer to "programming languages". Really, the best fit would be a presentation of a category (with suitable structure). We can talk about, e.g. the free cartesian closed category generated from a graph.
When we want to talk about cartesian closed categories in general, we typically work with some presentation of them. Usually this happens by asserting that not only do certain universal constructions, e.g. binary products, exist, but that they are chosen by which we mean we have a (bi)functor that actually picks out a specific object to be the binary product of two other objects. This chosen structure, particularly combined with a presentation for the underlying category, provides an abstract, syntactical way of referring to structure within an arbitrary cartesian closed category. It is possible to compile the simply typed lambda calculus (STLC) in terms of this structure in such a way as to validate the reduction rules of the STLC. We can go further and show that all that structure is expressible in terms of the syntax of the STLC in such a way as to validate the universal properties. Altogether this leads to the simply typed lambda calculus being the internal language of cartesian closed categories. This is indeed part of the Curry-Howard-Lambek correspondence.
I haven't watched the video you reference, but there's definitely a way it can be understood to be roughly true. Erik Meijer does know what he's talking about to a reasonable degree with regards to these topics. However, he's often talking to an audience where there's not much value in being very precise.
answered Jan 27 at 11:05
Derek ElkinsDerek Elkins
17.3k11437
$endgroup$
add a comment |
$begingroup$
It would make more sense to say that categories are the semantic domains for denotational semantics for type theories (or rather, serve that function rather well). In other words, it would make more sense to say that if you were trying to understand the meaning of a program, you could interpret it into objects and arrows of a category with suitable structure, and then analyze the result mathematically. That said, you can formulate syntactic categories that, as the name suggests, are closer to "programming languages". Really, the best fit would be a presentation of a category (with suitable structure). We can talk about, e.g. the free cartesian closed category generated from a graph.
When we want to talk about cartesian closed categories in general, we typically work with some presentation of them. Usually this happens by asserting that not only do certain universal constructions, e.g. binary products, exist, but that they are chosen by which we mean we have a (bi)functor that actually picks out a specific object to be the binary product of two other objects. This chosen structure, particularly combined with a presentation for the underlying category, provides an abstract, syntactical way of referring to structure within an arbitrary cartesian closed category. It is possible to compile the simply typed lambda calculus (STLC) in terms of this structure in such a way as to validate the reduction rules of the STLC. We can go further and show that all that structure is expressible in terms of the syntax of the STLC in such a way as to validate the universal properties. Altogether this leads to the simply typed lambda calculus being the internal language of cartesian closed categories. This is indeed part of the Curry-Howard-Lambek correspondence.
I haven't watched the video you reference, but there's definitely a way it can be understood to be roughly true. Erik Meijer does know what he's talking about to a reasonable degree with regards to these topics. However, he's often talking to an audience where there's not much value in being very precise.
answered Jan 27 at 11:05
Derek ElkinsDerek Elkins
17.3k11437
$endgroup$
add a comment |
$begingroup$
It would make more sense to say that categories are the semantic domains for denotational semantics for type theories (or rather, serve that function rather well). In other words, it would make more sense to say that if you were trying to understand the meaning of a program, you could interpret it into objects and arrows of a category with suitable structure, and then analyze the result mathematically. That said, you can formulate syntactic categories that, as the name suggests, are closer to "programming languages". Really, the best fit would be a presentation of a category (with suitable structure). We can talk about, e.g. the free cartesian closed category generated from a graph.
When we want to talk about cartesian closed categories in general, we typically work with some presentation of them. Usually this happens by asserting that not only do certain universal constructions, e.g. binary products, exist, but that they are chosen by which we mean we have a (bi)functor that actually picks out a specific object to be the binary product of two other objects. This chosen structure, particularly combined with a presentation for the underlying category, provides an abstract, syntactical way of referring to structure within an arbitrary cartesian closed category. It is possible to compile the simply typed lambda calculus (STLC) in terms of this structure in such a way as to validate the reduction rules of the STLC. We can go further and show that all that structure is expressible in terms of the syntax of the STLC in such a way as to validate the universal properties. Altogether this leads to the simply typed lambda calculus being the internal language of cartesian closed categories. This is indeed part of the Curry-Howard-Lambek correspondence.
I haven't watched the video you reference, but there's definitely a way it can be understood to be roughly true. Erik Meijer does know what he's talking about to a reasonable degree with regards to these topics. However, he's often talking to an audience where there's not much value in being very precise.
answered Jan 27 at 11:05
Derek ElkinsDerek Elkins
17.3k11437
$endgroup$
It would make more sense to say that categories are the semantic domains for denotational semantics for type theories (or rather, serve that function rather well). In other words, it would make more sense to say that if you were trying to understand the meaning of a program, you could interpret it into objects and arrows of a category with suitable structure, and then analyze the result mathematically. That said, you can formulate syntactic categories that, as the name suggests, are closer to "programming languages". Really, the best fit would be a presentation of a category (with suitable structure). We can talk about, e.g. the free cartesian closed category generated from a graph.
When we want to talk about cartesian closed categories in general, we typically work with some presentation of them. Usually this happens by asserting that not only do certain universal constructions, e.g. binary products, exist, but that they are chosen by which we mean we have a (bi)functor that actually picks out a specific object to be the binary product of two other objects. This chosen structure, particularly combined with a presentation for the underlying category, provides an abstract, syntactical way of referring to structure within an arbitrary cartesian closed category. It is possible to compile the simply typed lambda calculus (STLC) in terms of this structure in such a way as to validate the reduction rules of the STLC. We can go further and show that all that structure is expressible in terms of the syntax of the STLC in such a way as to validate the universal properties. Altogether this leads to the simply typed lambda calculus being the internal language of cartesian closed categories. This is indeed part of the Curry-Howard-Lambek correspondence.
I haven't watched the video you reference, but there's definitely a way it can be understood to be roughly true. Erik Meijer does know what he's talking about to a reasonable degree with regards to these topics. However, he's often talking to an audience where there's not much value in being very precise.
answered Jan 27 at 11:05
Derek ElkinsDerek Elkins
17.3k11437
answered Jan 27 at 11:05
Derek ElkinsDerek Elkins
17.3k11437
answered Jan 27 at 11:05
Derek ElkinsDerek Elkins
17.3k11437
answered Jan 27 at 11:05
Derek ElkinsDerek Elkins
17.3k11437
17.3k11437
add a comment |
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%2f3089336%2fcan-we-see-categories-as-programming-languages%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$
Functional programming goes in this direction.
$endgroup$
– Wuestenfux
Jan 27 at 9:35
$begingroup$
You could also explain category theory to a person having only a hammer by saying that objects are nails ...
$endgroup$
– Hagen von Eitzen
Jan 27 at 9:38