## From tries to trees

This post is the last of a series of six relating numbers, vectors, and trees, revolving around the themes of static size-typing and memo tries. We’ve seen that length-typed vectors form a trie for bounded numbers, and can handily represent numbers as well. We’ve also seen that n-dimensional vectors themselves have an elegant trie, which is the n-ary composition of the element type’s trie functor:

``type VTrie n a = Trie a :^ n ``

where for any functor `f` and natural number type `n`,

``f :^ n ≅ f ∘ ⋯ ∘ f  -- (n times)``

This final post in the series places this elegant mechanism of n-ary functor composition into a familiar & useful context, namely trees. Again, type-encoded Peano numbers are central. Just as `BNat` uses these number types to (statically) bound natural numbers (e.g., for a vector index or a numerical digit), and `Vec` uses number types to capture vector length, we’ll next use number types to capture tree depth.

Edits:

• 2011-02-02: Changes thanks to comments from Sebastian Fischer
• Added pointer to Memoizing polymorphic functions via unmemoization for derivation of `Tree d a ≅ [d] → a`.
• Fixed signatures for some `Branch` variants, bringing type parameter `a` into parens.
• Clarification about number of `VecTree` vs pairing constructors in remarks on left- vs right-folded trees.
• 2011-02-06: Fixed link to From Fast Exponentiation to Square Matrices.

Continue reading ‘From tries to trees’ »

## 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.

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?

Edits:

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

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

## Doing more with length-typed vectors

The post Fixing lists defined a (commonly used) type of vectors, whose lengths are determined statically, by type. In `Vec n a`, the length is `n`, and the elements have type `a`, where `n` is a type-encoded unary number, built up from zero and successor (`Z` and `S`).

``infixr 5 :<data Vec ∷ * → * → * where  ZVec ∷                Vec Z     a  (:<) ∷ a → Vec n a → Vec (S n) a``

It was fairly easy to define `foldr` for a `Foldable` instance, `fmap` for `Functor`, and `(⊛)` for `Applicative`. Completing the `Applicative` instance is tricky, however. Unlike `foldr`, `fmap`, and `(⊛)`, `pure` doesn’t have a vector structure to crawl over. It must create just the right structure anyway. I left this challenge as a question to amuse readers. In this post, I give a few solutions, including my current favorite.

You can find the code for this post and the two previous ones in a code repository.

Continue reading ‘Doing more with length-typed vectors’ »

## Fixing lists

In the post Memoizing polymorphic functions via unmemoization, I toyed with the idea of lists as tries. I don’t think `[a]` is a trie, simply because `[a]` is a sum type (being either nil or a cons), while tries are built out of the identity, product, and composition functors. In contrast, `Stream` is a trie, being built solely with the identity and product functors. Moreover, `Stream` is not just any old trie, it is the trie that corresponds to Peano (unary natural) numbers, i.e., `Stream a ≅ N → a`, where

``data N = Zero | Succ Ndata Stream a = Cons a (Stream a)``

If we didn’t already know the `Stream` type, we would derive it systematically from `N`, using standard isomorphisms.

`Stream` is a trie (over unary numbers), thanks to it having no choice points, i.e., no sums in its construction. However, streams are infinite-only, which is not always what we want. In contrast, lists can be finite, but are not a trie in any sense I understand. In this post, I look at how to fix lists, so they can be finite and yet be a trie, thanks to having no choice points (sums)?

You can find the code for this post and the previous one in a code repository.

Edits: