KnownNat-indexed vectors

The function is more like an interface compared to an array, which is an implementation. iirc, “Algebra Driven Design” has a whole part where it discusses using functions like this. This style is what puts the F in FP. I rarely see it in industry sadly. Industrial Haskell smells more like Java than Scheme