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

$\endgroup$
  • $\begingroup$ They're in the closet. $\endgroup$ – Andrej Bauer Jan 27 at 8:10
11
$\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.

$\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$ – BalancedTryteOperators Jan 25 at 23:31
  • 2
    $\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 $\lambda\omega$-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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.