Yes, you really need at least Pi types (dependent products, as above) or Sigma types (dependent pairs) to have dependent types. So you could get away with it in

Yes, you really need at least Pi types (dependent products, as above) or Sigma types (dependent pairs) to have dependent types. So you could get away with it in Python by munging a return type based on a parameter, but not C++ or most other statically typed languages! 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.