4 ms·
The n can come from the database, a file, or even user input from a text box. That's the point of dependent types: types can depend on run-time values.
by jules 12y ago
The n can come from the database, a file, or even user input from a text box. That's the point of dependent types: types can depend on run-time values.
- tel 12y agoWell, the n must "come from" the actual data. You could not construct a vector of any other size n. It'll just be typed so as to be realized at runtime and then maintained. The functions by-and-large do not ensure that the vector is sized for a particular n, but instead that they respect whatever n ends up being true.