Archive for 31st January 2011

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?


  • 2011-01-31: Switched trie notation to "k ↛ v" to avoid missing character on iPad.

Continue reading ‘A trie for length-typed vectors’ »

Reverse-engineering length-typed vectors

The last few posts posts followed a winding path toward a formulation of a type for length-typed vectors. In Fixing lists, I mused how something like lists could be a trie type. The Stream functor (necessarily infinite lists) is the natural trie for Peano numbers. The standard list functor [] (possibly finite lists) doesn’t seem to be a trie, since it’s built from sums. However, the functor Vec n of vectors ("fixed lists") of length n is built from (isomorphic to) products only (for any given n), and so might well be a trie.

Of what type is Vec n the corresponding trie? In other words, for what type q is Vec n a isomorphic to q → a (for all a).

Turning this question on its head, what simpler type gives rise to length-typed vectors in a standard fashion?


  • 2011-02-01: Define Digits n b as BNat n ↛ BNat b.

Continue reading ‘Reverse-engineering length-typed vectors’ »