▲ | Rusky 4 months 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 4 months ago | parent [-] | |||||||||||||||||||||||||
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. | ||||||||||||||||||||||||||
|