Mixing
Where are C++ templates inside of the lambda cube?
$begingroup$
C++ templates have type variables and can express lambdas, so they must have System F embedded. But is that exactly where they are located in the lambda cube? Can C++ templates produce new types or express dependent types?
(I originally posted this to Stack Overflow, but they referred me over to here.)
programming-languages type-theory dependent-types c++ calculus-of-constructions
edited Jan 26 at 14:30
Raphael♦
57.9k24142317
asked Jan 25 at 20:00
Tomislav OstojichTomislav Ostojich
19815
$endgroup$
add a comment |
$begingroup$
C++ templates have type variables and can express lambdas, so they must have System F embedded. But is that exactly where they are located in the lambda cube? Can C++ templates produce new types or express dependent types?
(I originally posted this to Stack Overflow, but they referred me over to here.)
programming-languages type-theory dependent-types c++ calculus-of-constructions
edited Jan 26 at 14:30
Raphael♦
57.9k24142317
asked Jan 25 at 20:00
Tomislav OstojichTomislav Ostojich
19815
$endgroup$
$begingroup$
They're in the closet.
$endgroup$
– Andrej Bauer
Jan 27 at 8:10
add a comment |
$begingroup$
C++ templates have type variables and can express lambdas, so they must have System F embedded. But is that exactly where they are located in the lambda cube? Can C++ templates produce new types or express dependent types?
(I originally posted this to Stack Overflow, but they referred me over to here.)
programming-languages type-theory dependent-types c++ calculus-of-constructions
edited Jan 26 at 14:30
Raphael♦
57.9k24142317
asked Jan 25 at 20:00
Tomislav OstojichTomislav Ostojich
19815
$endgroup$
C++ templates have type variables and can express lambdas, so they must have System F embedded. But is that exactly where they are located in the lambda cube? Can C++ templates produce new types or express dependent types?
(I originally posted this to Stack Overflow, but they referred me over to here.)
programming-languages type-theory dependent-types c++ calculus-of-constructions
programming-languages type-theory dependent-types c++ calculus-of-constructions
edited Jan 26 at 14:30
Raphael♦
57.9k24142317
asked Jan 25 at 20:00
Tomislav OstojichTomislav Ostojich
19815
edited Jan 26 at 14:30
Raphael♦
57.9k24142317
asked Jan 25 at 20:00
Tomislav OstojichTomislav Ostojich
19815
edited Jan 26 at 14:30
Raphael♦
57.9k24142317
edited Jan 26 at 14:30
Raphael♦
57.9k24142317
edited Jan 26 at 14:30
Raphael♦
57.9k24142317
57.9k24142317
asked Jan 25 at 20:00
Tomislav OstojichTomislav Ostojich
19815
asked Jan 25 at 20:00
Tomislav OstojichTomislav Ostojich
19815
asked Jan 25 at 20:00
Tomislav OstojichTomislav Ostojich
19815
19815
$begingroup$
They're in the closet.
$endgroup$
– Andrej Bauer
Jan 27 at 8:10
add a comment |
$begingroup$
They're in the closet.
$endgroup$
– Andrej Bauer
Jan 27 at 8:10
$begingroup$
They're in the closet.
$endgroup$
– Andrej Bauer
Jan 27 at 8:10
$begingroup$
They're in the closet.
$endgroup$
– Andrej Bauer
Jan 27 at 8:10
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
But is that exactly where they are located in the lambda cube?
The lambda cube is not a giant spectrum on which all programming languages can be classified. It is precisely eight languages, which combine a lambda calculus (values abstracted over values) with all possible combinations of three features:
- Values abstracted over types (parametric polymorphism)
- Types abstracted over types (kinds / type constructors)
- Types abstracted over values (dependent types)
So, the C++ template language isn't anywhere on the lambda cube, since it isn't any of those 8 languages.
The second thing to keep in mind is that we can't mix up C++ features and C++ template features. Just because C++ has lambdas, this doesn't (necessarily) mean that its template language has them.
It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure.
answered Jan 25 at 22:01
jmitejmite
22.9k347100
$endgroup$
1
$begingroup$
"It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure." This is the question I meant to ask! And thank you for providing an answer in the form of a demonstration/proof.
$endgroup$
– Tomislav Ostojich
Jan 25 at 23:31
1
$begingroup$
I'm pretty sure that C++ example does not indicate that it has all the features of the lambda cube. The majority of it is doing completely normal functional programming via constexprs and template. That is, the source material is just functional programming. The only exception is the one Theorem and one Lemma at the bottom, but it's not clear to me either the source or the translation are an adequate example of dependent typing. The listing mostly demonstrates $lambdaomega$-style features and not parametric polymorphism nor dependent typing.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
$begingroup$
There are issues with even viewing straightforward uses of C++ templates as parametric polymorphism, but they may not be a problem for this particular context.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
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: "419"
};
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: false,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: null,
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
},
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%2fcs.stackexchange.com%2fquestions%2f103401%2fwhere-are-c-templates-inside-of-the-lambda-cube%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$
But is that exactly where they are located in the lambda cube?
The lambda cube is not a giant spectrum on which all programming languages can be classified. It is precisely eight languages, which combine a lambda calculus (values abstracted over values) with all possible combinations of three features:
- Values abstracted over types (parametric polymorphism)
- Types abstracted over types (kinds / type constructors)
- Types abstracted over values (dependent types)
So, the C++ template language isn't anywhere on the lambda cube, since it isn't any of those 8 languages.
The second thing to keep in mind is that we can't mix up C++ features and C++ template features. Just because C++ has lambdas, this doesn't (necessarily) mean that its template language has them.
It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure.
answered Jan 25 at 22:01
jmitejmite
22.9k347100
$endgroup$
1
$begingroup$
"It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure." This is the question I meant to ask! And thank you for providing an answer in the form of a demonstration/proof.
$endgroup$
– Tomislav Ostojich
Jan 25 at 23:31
1
$begingroup$
I'm pretty sure that C++ example does not indicate that it has all the features of the lambda cube. The majority of it is doing completely normal functional programming via constexprs and template. That is, the source material is just functional programming. The only exception is the one Theorem and one Lemma at the bottom, but it's not clear to me either the source or the translation are an adequate example of dependent typing. The listing mostly demonstrates $lambdaomega$-style features and not parametric polymorphism nor dependent typing.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
$begingroup$
There are issues with even viewing straightforward uses of C++ templates as parametric polymorphism, but they may not be a problem for this particular context.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
add a comment |
$begingroup$
But is that exactly where they are located in the lambda cube?
The lambda cube is not a giant spectrum on which all programming languages can be classified. It is precisely eight languages, which combine a lambda calculus (values abstracted over values) with all possible combinations of three features:
- Values abstracted over types (parametric polymorphism)
- Types abstracted over types (kinds / type constructors)
- Types abstracted over values (dependent types)
So, the C++ template language isn't anywhere on the lambda cube, since it isn't any of those 8 languages.
The second thing to keep in mind is that we can't mix up C++ features and C++ template features. Just because C++ has lambdas, this doesn't (necessarily) mean that its template language has them.
It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure.
answered Jan 25 at 22:01
jmitejmite
22.9k347100
$endgroup$
1
$begingroup$
"It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure." This is the question I meant to ask! And thank you for providing an answer in the form of a demonstration/proof.
$endgroup$
– Tomislav Ostojich
Jan 25 at 23:31
1
$begingroup$
I'm pretty sure that C++ example does not indicate that it has all the features of the lambda cube. The majority of it is doing completely normal functional programming via constexprs and template. That is, the source material is just functional programming. The only exception is the one Theorem and one Lemma at the bottom, but it's not clear to me either the source or the translation are an adequate example of dependent typing. The listing mostly demonstrates $lambdaomega$-style features and not parametric polymorphism nor dependent typing.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
$begingroup$
There are issues with even viewing straightforward uses of C++ templates as parametric polymorphism, but they may not be a problem for this particular context.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
add a comment |
$begingroup$
But is that exactly where they are located in the lambda cube?
The lambda cube is not a giant spectrum on which all programming languages can be classified. It is precisely eight languages, which combine a lambda calculus (values abstracted over values) with all possible combinations of three features:
- Values abstracted over types (parametric polymorphism)
- Types abstracted over types (kinds / type constructors)
- Types abstracted over values (dependent types)
So, the C++ template language isn't anywhere on the lambda cube, since it isn't any of those 8 languages.
The second thing to keep in mind is that we can't mix up C++ features and C++ template features. Just because C++ has lambdas, this doesn't (necessarily) mean that its template language has them.
It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure.
answered Jan 25 at 22:01
jmitejmite
22.9k347100
$endgroup$
But is that exactly where they are located in the lambda cube?
The lambda cube is not a giant spectrum on which all programming languages can be classified. It is precisely eight languages, which combine a lambda calculus (values abstracted over values) with all possible combinations of three features:
- Values abstracted over types (parametric polymorphism)
- Types abstracted over types (kinds / type constructors)
- Types abstracted over values (dependent types)
So, the C++ template language isn't anywhere on the lambda cube, since it isn't any of those 8 languages.
The second thing to keep in mind is that we can't mix up C++ features and C++ template features. Just because C++ has lambdas, this doesn't (necessarily) mean that its template language has them.
It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure.
answered Jan 25 at 22:01
jmitejmite
22.9k347100
answered Jan 25 at 22:01
jmitejmite
22.9k347100
answered Jan 25 at 22:01
jmitejmite
22.9k347100
answered Jan 25 at 22:01
jmitejmite
22.9k347100
22.9k347100
1
$begingroup$
"It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure." This is the question I meant to ask! And thank you for providing an answer in the form of a demonstration/proof.
$endgroup$
– Tomislav Ostojich
Jan 25 at 23:31
1
$begingroup$
I'm pretty sure that C++ example does not indicate that it has all the features of the lambda cube. The majority of it is doing completely normal functional programming via constexprs and template. That is, the source material is just functional programming. The only exception is the one Theorem and one Lemma at the bottom, but it's not clear to me either the source or the translation are an adequate example of dependent typing. The listing mostly demonstrates $lambdaomega$-style features and not parametric polymorphism nor dependent typing.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
$begingroup$
There are issues with even viewing straightforward uses of C++ templates as parametric polymorphism, but they may not be a problem for this particular context.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
add a comment |
1
$begingroup$
"It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure." This is the question I meant to ask! And thank you for providing an answer in the form of a demonstration/proof.
$endgroup$
– Tomislav Ostojich
Jan 25 at 23:31
1
$begingroup$
I'm pretty sure that C++ example does not indicate that it has all the features of the lambda cube. The majority of it is doing completely normal functional programming via constexprs and template. That is, the source material is just functional programming. The only exception is the one Theorem and one Lemma at the bottom, but it's not clear to me either the source or the translation are an adequate example of dependent typing. The listing mostly demonstrates $lambdaomega$-style features and not parametric polymorphism nor dependent typing.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
$begingroup$
There are issues with even viewing straightforward uses of C++ templates as parametric polymorphism, but they may not be a problem for this particular context.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
1
1
$begingroup$
"It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure." This is the question I meant to ask! And thank you for providing an answer in the form of a demonstration/proof.
$endgroup$
– Tomislav Ostojich
Jan 25 at 23:31
$begingroup$
"It is possible to ask, which of the three lambda-cube features does C++ have? It would seem that it features the full power of the lambda cube, but I'm not enough of a C++ expert to know for sure." This is the question I meant to ask! And thank you for providing an answer in the form of a demonstration/proof.
$endgroup$
– Tomislav Ostojich
Jan 25 at 23:31
1
1
$begingroup$
I'm pretty sure that C++ example does not indicate that it has all the features of the lambda cube. The majority of it is doing completely normal functional programming via constexprs and template. That is, the source material is just functional programming. The only exception is the one Theorem and one Lemma at the bottom, but it's not clear to me either the source or the translation are an adequate example of dependent typing. The listing mostly demonstrates $lambdaomega$-style features and not parametric polymorphism nor dependent typing.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
$begingroup$
I'm pretty sure that C++ example does not indicate that it has all the features of the lambda cube. The majority of it is doing completely normal functional programming via constexprs and template. That is, the source material is just functional programming. The only exception is the one Theorem and one Lemma at the bottom, but it's not clear to me either the source or the translation are an adequate example of dependent typing. The listing mostly demonstrates $lambdaomega$-style features and not parametric polymorphism nor dependent typing.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
$begingroup$
There are issues with even viewing straightforward uses of C++ templates as parametric polymorphism, but they may not be a problem for this particular context.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
$begingroup$
There are issues with even viewing straightforward uses of C++ templates as parametric polymorphism, but they may not be a problem for this particular context.
$endgroup$
– Derek Elkins
Jan 26 at 1:31
add a comment |
Thanks for contributing an answer to Computer Science 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%2fcs.stackexchange.com%2fquestions%2f103401%2fwhere-are-c-templates-inside-of-the-lambda-cube%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
$begingroup$
They're in the closet.
$endgroup$
– Andrej Bauer
Jan 27 at 8:10