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
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.
- 2011-02-02: Changes thanks to comments from Sebastian Fischer
- Added note about number representations and leading zeros (without size-typing).
- Added pointer to Memoizing polymorphic functions via unmemoization for derivation of
Tree d a ≅ [d] → a.
- Fixed signatures for some
Branchvariants, bringing type parameter
- Clarification about number of
VecTreevs pairing constructors in remarks on left- vs right-folded trees.
- 2011-02-06: Fixed link to From Fast Exponentiation to Square Matrices.