Conal Elliott

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 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 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’ »

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