3 ms·
I really like your examples with the vector whose size is controlled by the type. However, is that useful in practice? I suppose that your vector would be read
by S4M 12y ago
I really like your examples with the vector whose size is controlled by the type. However, is that useful in practice? I suppose that your vector would be read from a file or a database (especially if you do data analysis), in which case you can't know in advance - at compile time - what size the vectors will have.
I suppose it can still work if you want to do things with the covariance/correlation matrix: you may not know the number of rows before hand, but you know the number of columns, or know that two data sets will have the same number of columns.
- tel 12y agoThe code you write doesn't necessarily fix an n, it just says that n cannot change in unprincipled ways throughout a computation. When you read in a vector from a database it will originally be unsized, but you can write code that shows the size is computed and left fixed and then from then on treat it as a sized vector. It's hard to say exactly how useful this is in practice. More honestly, this is a rather trivial example mostly used to demonstrate DT. One use of it is in implementing de Bruijn indexed lambda calculus interpreters---if you let the environment be a sized vector then you can use `n` to ensure there aren't bad variables in scope and to take note of closed expressions.
- jules 12y agoThe 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.