As net4all pointed out, your C++ example isn't really dependent types. It's achievable with parametric polymorphism a la System F, AKA the ML-style or Java-styl

As net4all pointed out, your C++ example isn't really dependent types. It's achievable with parametric polymorphism a la System F, AKA the ML-style or Java-style generics. C++ does have value arguments for templates, however. Perhaps a better example would have been std::array, which takes a size as an argument. However, C++ still doesn't really have dependent types the same way Agda or Idris has them. One big difference is that C++ templates are only checked upon instantiation. So, this code: template<typename T, T a> std::array<int, a + 1> add() { return {1, 2}; } compiles, but when I try to do add<int, 0>() the compiler complains. Because the dependent function type means "forall," it's important that the compiler make sure that it truly does work for all inputs.