I’m pretty excited to present you fast-vect.
tl;dr
A vector (not to be confounded with C++/Rust-style vectors) is a list that has its size encoded in its type:
vect :: Vect "1" String
vect = singleton "a"
Check out the screencast here:
Long story
This library provides Idris-style vectors that have their size encoded in the type. Why is this useful? Because the compiler can catch errors, e.g. when you try to access the element at index 10 in a 10 element vector:
vect :: Vect "10" String
vect = replicate (term :: _ "10") "a"
-- last = index (term :: _ "10") vect -- compile-time error
last = index (term :: _ "9") vect
first = index (term :: _ "0") vect
Some examples of use-cases:
- Ensure that your ML model has the correct amount of elements
- Crypto libraries require keys and initialization vectors have a certain size
- Make sure that your layout grid has the right amount of columns
There are a few vector implementations in Purescript already, but they all use natural (peano) numbers to encode the size (remember a natural number is defined as either zero Z or the successor of a previous number S k).
The problem with this is, that this gets very slow very quickly to the point that they are not usable anymore. E.g. using the purescript peano library to add 500 to 500 took about a minute on my machine. Idris2 vectors blew up when the size got to about ten million (I haven’t done proper benchmarks though…).
A second problem is that this is not readable anymore, because e.g. a ten elements vector will be represented like this Vect (S (S (S (S (S (S (S (S (S (S Z)))))))))) Int.
In contrast this library uses symbols to encode the size and high-school arithmetic to do the calculations. This turned out to be pretty fast and is also human-readable.