> Let’s consider an application, for example, in computer graphics, in which we have potentially many pairs of vectors of the fixed (but statically unknown) length and a function—such as vector addition—to be applied to them.
> This function should be fast because it is applied many times and be safe because just one runtime error may ruin the whole long-running calculation.
> Our goal is to define the function `vadd` of type $$Πn : Int.∀β.⊲β(Vector (\%_αn) → Vector (\%_αn) → Vector (\%_αn))$$
> .It takes the length n and returns (β-closed) code of a function to add two vectors of length n. The generated code is run by applying it to ε to obtain a function of type $Vector\; n → Vector\; n → Vector\; n$ as expected.
