vector-sized

This package exports a newtype tagging the vectors from the vector package with a type-level natural representing their size. It also exports functions from vector whose size can be determined ahead of time, appropriately retyped.

Currently, we provide size-tagged versions of the following:

• Data.Vector.Vector, in Data.Vector.Sized
• Data.Vector.Generic.Vector, in Data.Vector.Generic.Sized
• Data.Vector.Storable.Vector, in Data.Vector.Storable.Sized
• Data.Vector.Unboxed.Vector, in Data.Vector.Unboxed.Sized

We also provide mutable versions of each of the above. Additionally, we include functions for converting to and from 'unsized' vectors and lists, using CPS-style existentials.

The code in this package is based on the initial work by Ben Gamari in a PR for vulkan.

How is this different to fixed-vector?

This package is fairly similar to fixed-vector, as both libraries are designed to provide vectors of statically known length. However, the implementations used are different, with different tradeoffs. vector-sized uses a newtype wrapper around vectors from vector, and is thus able to handle vectors of arbitrary length. However, this approach requires us to carry a runtime representation of length, which is a significant memory overhead for small vectors. fixed-vector instead defines all functions as manipulations of Church-encoded product types of the form ∀r. (a → a → r) → r (for 2D vectors), allowing it to work for both arbitrary product types (like data V2 a = V2 a a) and opaque length-parameterized vectors. However, as a consequence of this implementation choice, fixed-vector cannot handle vectors whose size exceeds tens of elements.