C++ and the lambda cube

So the three axes of the lambda cube are:

• Types depending on types
• Terms depending on types
• Types depending on terms

(If you don't have terms depending on terms, you don't have a programming language at all, really.)

C++ appears to have all three, but doesn't really. I shall elucidate.

• Types depending on types are simple: those are any form of type constructor of kind * -> *. Specifically, int *, int class A::*, and std::vector<int> are all examples of type constructors applied to int.
• Terms depending on types are in general less familiar to novice C++ programmers, but are still well-known: the humble sizeof (present since C) is an example of this. User-defined type-to-term "functions" are also possible:
  
template <typename T> class is_int { static const bool value = false; };
template <> class is_int<int> { static const bool value = true; };

assert(is_int<int>::value);
assert(!is_int<long>::value);
• Types depending on terms would seem to exist: the template std::array takes an argument of type std::size_t — e.g., std::array<int, sizeof(long)+6*7>.

However, this last one merely relies on an implicit hoisting into the type-system of integers and their operations. That is, for each integer value of each integral type, there is a basic unnamable type corresponding to that integer and that integer alone; and there are metaoperations defined across those types to produce each other. (Haskell does this sort of thing all the time as an exercise.) The constexpr extension in C++0x will allow users to easily define type metaoperations. (This was already possible, of course — see, e.g., Boost.MPL — it will now merely be easier.)

The presence of this dichotomy is evident from the fact that, while the above declaration of std::array is legal, the simpler int n = 0; std::array<int, n> is impossible to compile. "Types depending on terms" is not something that a statically typed language can easily have, if at all.

Because of inheritance and subtyping, it is possible for the underlying type of an object to depend on the value of a term; but the structural type of that object will still be fixed, being at most the supertype (limit superior) of all the underlying concrete types it could be. In a language like C++, where there is no ultimate supertype, you cannot have a function that returns, directly, either an int or a float depending on the values of its parameters.

Not that I can imagine ever wanting to. I'm just saying.