galangalalgol 3 days ago

In c++ it does care what N and M are at compile time, at least the optimizer does for autovectorization and unrolling. Would that not be the case with const generic expressions?

1
Rusky 2 days ago

The question of whether a language is dependently typed only has to do with how type checking is done. The optimizer doesn't come into play until later, so whether it uses the information is unrelated to whether the language is dependently typed.

galangalalgol 2 days ago

Ok, I think I understand now, but is it really dependently typed just because it symbolically verified it can work with any N and M? Because it will only generate code for the instantiations that get used at compile time.

Rusky 1 day ago

Is what really dependently typed? I'm saying C++ is not dependently typed, because it doesn't do any symbolic verification of N and M.

galangalalgol 1 day ago

If rust did add const generic expressions I mean. It still would only generate code for the used instantiations.

Rusky 1 day ago

Ah, I wasn't really talking about Rust.

Rust already does have some level of const generic expressions, but they are indeed only possible to instantiate with values known at compile time, like C++.

The difficulty of type checking them symbolically still applies regardless of how they're instantiated, but OTOH it doesn't look like Rust is really trying to go that direction.