template <typename T, int N> struct vec { T data[N]; };
vec<T,n> repeat(int n, T const& x) {...}
Note the run-time value n appearing in the return type of `repeat`. Because of this, repeat (if we could write it) has a dependent product type: the actual return type varies based on an argument's value.Unfortunately it seems like there is a lot of fog around this. Even the wikipedia page for dependent types botches the first example: "pairs of numbers where the second element is greater than the first" is just a normal type. A dependent type would be something like "pair<int,vec<T,n>>" where the n is supposed to equal the first element of the pair.
The waters are muddied even further by the fact that you can reproduce many of the canonical examples for dependent types using other mechanisms, as you pointed out below for the vector-append operation!
Edit: After complaining a bit about the Wikipedia page, it was pointed out that you can think of that example as a Sigma type. I contend it is not obvious unless you have already spent time thinking about dependent types, though.
Sometimes it feels like a kludge, but then I get to enjoy the nice IDEs, libraries that it has.
If only C++ had proper pattern matching support.
Of course, it isn't the only language I play with.
A prototypical concept you would expect to find in a dependently typed language is "the ability to have a function that concatenates to arrays of sizes X and Y and returns an array of size X+Y that can be safely verified against further functions that also require arrays given as arguments to have specific lengths".
C++ is a bit indirect in its semantics here, but you will note that most other languages with generic types cannot express this thought (using either real integers or simulating them with types, either of which can be done in C++).
One could easily imagine "filling out" C++ to allow compile time type argument manipulation of more value types without even stressing its model, and in fact that is exactly the direction the language has been going in with constexpr. Here is an article on how to build a compile-time printf using C++14.
http://blogs.microsoft.co.il/sasha/2015/01/29/compile-time-r...
The only real limitation in C++ is that these values have to be relatively "concrete": at some level there has to be a number that can be calculated, as you can only deal with values as you don't have the amazing ability to do unification of program fragments like you have access to in Idris (like, you'd like to be able to say "the length of this array is the same as the length of this runtime string", and then after a bunch of array manipulation claim that you return a string five characters longer than the input string). Again, though: this could be added to C++ without breaking its underlying model. And it definitely is not required by the concept of "dependent types" [edit: matt-noonan points out it is, in fact, required for a language to have "dependent types" :(.]