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

"Incorrect syntax near the keyword 'ON'. (on update cascade, on delete cascade,)

Image
.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty{ height:90px;width:728px;box-sizing:border-box; } 2 total noob sorry any help greatly appreciated. I keep getting this "Incorrect syntax near the keyword 'ON'." heres my codes code one CREATE TABLE supplier ( supplierID INT PRIMARY KEY, ISBN INT FOREIGN KEY REFERENCES book(ISBN), price DECIMAL (5,2), ON UPDATE CASCADE, ON DELETE CASCADE, ); code two CREATE TABLE orders ( orderID INT PRIMARY KEY, customerID INT FOREIGN KEY REFERENCES customer(customerID), ISBN INT FOREIGN KEY REFERENCES book(ISBN), orderDate date, ON UPDATE CASCADE, ON DELETE CASCADE, ); Ive run out of stuff to try other than dumbing it down to uselessness.
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

RAC Tourist Trophy

Image
Pour les articles homonymes, voir Tourist Trophy. Le RAC Tourist Trophy est une course automobile organisée par le Royal Automobile Club d'Angleterre. Créée en 1905, cette course a fait partie des épreuves comptant pour le championnat du monde des voitures de sport entre 1953 et 1955, en 1958 et 1959, et entre 1962 et 1965. Après une interruption de 17 ans (l'épreuve s'arrête après 1988), le RAC Tourist Trophy reprend en 2005 sous l'égide de la FIA GT. Palmarès | John Napier sur Arrol-Johnston, vainqueur du premier RAC Tourist Trophy, en 1905. L'honorable C.S. Rolls, vainqueur du RAC Tourist Trophy 1906. Ernest Curtis, sur Rover 20 hp, vainqueur du RAC Tourist Trophy 1907. William Watson, vainqueur du RAC Tourist Trophy 1908. Kenelm Lee Guinness, vainqueur du RAC Tourist Trophy 1914 sur Sunbeam. Départ du RAC Tourist Trophy 1928. Louis Gérard, vainqueur du RAC Tourist Trophy 1938 sur Delage. Année Circuit Vainqueur
Read more