jcelerier 2 days ago

the only thing needed here is to be able to lift N & M from run-time to the type system (which in C++ as it stands exists only at compile-time). For "small" values of N&M that's doable with switches and instantiations for instance.

1
Rusky 1 day ago

The point of dependent types is to check these uses of N and M at compile time symbolically, for all possible values, without having to "lift" their actual concrete values to compile time.

Typical implementations of dependent types do not generate a separate copy of a function for every instantiation, the way C++ does, so they simply do not need the concrete values in the same way.