A trie for length-typed vectors
As you might have noticed, I’ve been thinking and writing about memo tries lately. I don’t mean to; they just keep coming up.
Memoization is the conversion of functions to data structures. A simple, elegant, and purely functional form of memoization comes from applying three common type isomorphisms, which also correspond to three laws of exponents, familiar from high school math, as noted by Ralf Hinze in his paper Generalizing Generalized Tries.
In Haskell, one can neatly formulate memo tries via an associated functor, Trie, with a convenient synonym "k ↛ v" for Trie k v, as in Elegant memoization with higher-order types. (Note that I’ve changed my pretty-printing from "k :→: v" to "k ↛ v".) The key property is that the data structure encodes (is isomorphic to) a function, i.e.,
k ↛ a ≅ k → a
In most cases, we ignore non-strictness, though there is a delightful solution for memoizing non-strict functions correctly.
My previous four posts explored use of types to statically bound numbers and to determine lengths of vectors.
Just as (infinite-only) streams are the natural trie for unary natural numbers, we saw in Reverse-engineering length-typed vectors that length-typed vectors (one-dimensional arrays) are the natural trie for statically bounded natural numbers.
BNat n ↛ a ≡ Vec n a
and so
BNat n → a ≅ Vec n a
In retrospect, this relationship is completely unsurprising, since a vector of length n is a collection of values, indexed by 0, . . . , n - 1.
In that same post, I noted that vectors are not only a trie for bounded numbers, but when the elements are also bounded numbers, the vectors can also be thought of as numbers. Both the number of digits and the number base are captured statically, in types:
type Digits n b = Vec n (BNat b)
The type parameters n and b here are type-encodigs of unary numbers, i.e., built up from zero and successor (Z and S). For instance, when b ≡ S (S Z), we have n-bit binary numbers.
In this new post, I look at another question of tries and vectors. Given that Vec n is the trie for BNat n, is there also a trie for Vec n?
Edits:
- 2011-01-31: Switched trie notation to "
k ↛ v" to avoid missing character on iPad.