This post is a follow-up to my fixed-length vectors in haskell in 2015 post! When I was writing the post originally, I was new to the whole type-level game in Haskell; I didn’t know what I was talking about, and that post was a way for me to push myself to learn more. Immediately after it was posted, of course, people taught me where I went wrong in the idioms I explained, and better and more idiomatic ways to do things. And that’s great! Learning is awesome!
Unfortunately, however, to my horror, I began noticing people referring to the post in a canonical/authoritative way…so the post became an immediate source of guilt to me. I tried correcting things with my practical dependent types in haskell series the next year. But I still saw my 2015 post being used as a reference even after that post, so I figured that writing a direct replacement/follow-up as the only way I would ever fix this!
So here we are in 2017. GHC 8.2 is here, and base is in version 4.10. What’s the “right” way to do fixed-length vectors in Haskell?
This post doesn’t attempt to present anything groundbreaking or new, but is meant to be a sort of reference/introduction to fixed-length vectors in Haskell, as of GHC 8.2 and the 2017 Haskell ecosystem.
We’ll be looking at two methods here: The first one we will be looking at is a performant fixed-length vector that you will probably be using for any code that requires a fixed-length container — especially for tight numeric code and situations where performance matters. We’ll see how to implement them using the universal native
KnownNat mechanisms, and also how we can implement them using singletons to help us make things a bit smoother and more well-integrated. For most people, this is all they actually need. (I claim the canonical haskell ecosystem source to be the vector-sized library)
The second method is a structural fixed-length inductive vector. It’s…actually more like a fixed-length (lazily linked) list than a vector. The length of the list is enforced by the very structure of the data type. This type is more useful as a streaming data type, and also in situations where you want take advantage of the structural characteristics of lengths in the context of a dependently typed program. (I claim the canonical haskell ecosystem source to be the type-combinators library)