The 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

The 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.