Where are C++ templates inside of the lambda cube?












5












$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







share|cite|improve this question











$endgroup$












  • $begingroup$
    They're in the closet.
    $endgroup$
    – Andrej Bauer
    20 hours ago


















5












$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







share|cite|improve this question











$endgroup$












  • $begingroup$
    They're in the closet.
    $endgroup$
    – Andrej Bauer
    20 hours ago
















5












5








5





$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







share|cite|improve this question











$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






share|cite|improve this question















share|cite|improve this question













share|cite|improve this question




share|cite|improve this question








edited yesterday









Raphael♦

57.5k23139315




57.5k23139315










asked 2 days ago









Tomislav OstojichTomislav Ostojich

1984




1984












  • $begingroup$
    They're in the closet.
    $endgroup$
    – Andrej Bauer
    20 hours ago




















  • $begingroup$
    They're in the closet.
    $endgroup$
    – Andrej Bauer
    20 hours ago


















$begingroup$
They're in the closet.
$endgroup$
– Andrej Bauer
20 hours ago






$begingroup$
They're in the closet.
$endgroup$
– Andrej Bauer
20 hours ago












1 Answer
1






active

oldest

votes


















10












$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.






share|cite|improve this answer









$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
    2 days ago






  • 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
    2 days ago










  • $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
    2 days ago











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
});


}
});














draft saved

draft discarded


















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









10












$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.






share|cite|improve this answer









$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
    2 days ago






  • 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
    2 days ago










  • $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
    2 days ago
















10












$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.






share|cite|improve this answer









$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
    2 days ago






  • 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
    2 days ago










  • $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
    2 days ago














10












10








10





$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.






share|cite|improve this answer









$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.







share|cite|improve this answer












share|cite|improve this answer



share|cite|improve this answer










answered 2 days ago









jmitejmite

22.6k34598




22.6k34598








  • 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
    2 days ago






  • 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
    2 days ago










  • $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
    2 days ago














  • 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
    2 days ago






  • 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
    2 days ago










  • $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
    2 days ago








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
2 days ago




$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
2 days ago




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
2 days ago




$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
2 days ago












$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
2 days ago




$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
2 days ago


















draft saved

draft discarded




















































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.




draft saved


draft discarded














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





















































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







-

Popular posts from this blog

If I really need a card on my start hand, how many mulligans make sense? [duplicate]

Image
5 This question already has an answer here: How do you calculate the likelihood of drawing certain cards in your opening hand? 3 answers There is a funny modern deck where you play Treasure Hunt, but you really need to have it on the starting hand. How many mulligans should I take, if my deck contains 60 cards and contains 4 copies of Treasure Hunt? magic-the-gathering probability share | improve this question asked Nov 23 '18 at 12:12 dan dan 152 4
Read more

Alcedinidae

Image
Alcedinidae Martin-pêcheur à dos bleu ( Alcedo azurea ) Classification (COI) Règne Animalia Embranchement Chordata Sous-embr. Vertebrata Classe Aves Ordre Coraciiformes Famille Alcedinidae Rafinesque, 1815 Les Alcédinidés ou Alcedinidae forment une famille d'oiseaux plus connus sous les noms de martins-pêcheurs et martins-chasseurs. Sommaire 1 Description 2 Répartition et habitat 3 Systématique 3.1 Liste alphabétique des genres 3.2 Liste des espèces 4 Chez les Anciens : l'alcyon 4.1 Étymologie (Littré) 4.2 Oiseau « fabuleux » ? 5 Notes 6 Articles connexes 7 Liens externes 7.1 Bibliographie Description | Ce sont des oiseaux compacts de taille petite à moyenne (10 à 46 cm), au bec droit et long, en forme de poignard. Leurs pattes sont courtes, et ils portent un plumage aux couleurs vives. Répartition et habitat | Cosmopolites, ils fréquentent surtout
Read more

Can an atomic nucleus contain both particles and antiparticles? [duplicate]

Image
9 $begingroup$ This question already has an answer here: What happens if we put together a proton and an antineutron? 2 answers Is it theoretically possible to make a "deuterium" atom containing a proton and an antineutron in its nucleus? Would the strong nuclear force cause attraction between a proton and an antineutron? Would such a nucleus be stable, or would the proton somehow annihilate the antineutron when close enough? nuclear-physics antimatter share | cite | improve this question asked yesterday
Read more