Fixed-length vector types (vector types that indicate the length of the vector in the type itself) are one of the more straightforward applications of the “super-Haskell” GHC type extensions. There’s a lot of magic you can do with GHC’s advanced type mechanisms, but I think fixed length vectors are a good first step to beginning to understand several extensions, including (potentially):
And using type system plugins. (And of course the usual
UndecidableInstances etc.) We’ll be discussing two different ways to implement this — using type-level nats, and using the GHC.TypeLits model to actually be able to use numeric literals in your types. These things are seen in the wild like with the popular linear package’s
There are a few great tutorials/writeups on this topic, but many of them are from the time before we had some of these extensions, or only discuss a few. I hope to provide a nice comprehensive look about the tools available today to really approach this topic. That being said, I am no expert myself, so I would appreciate any tips/edits/suggestions for things that I’ve missed or done not-the-best :) This post has a lot of open questions that I’m sure people who know more about this than me can answer.
Most of the code in this article can be downloaded and tried out, so follow along if you want!