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.
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
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
b here are type-encodigs of unary numbers, i.e., built up from zero and successor (
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
- 2011-01-31: Switched trie notation to "
k ↛ v" to avoid missing character on iPad.