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.

Deriving vectors

Recalling that Vec n a is an n-ary product of the type a, and forming the sort of derivation I used in Memoizing polymorphic functions via unmemoization,

Vec n a  a × ⋯ × a
(1 → a) × ⋯ × (1 → a)
(1 ++ 1) → a

where the type 1 is what we call "unit" or "()" in Haskell, having exactly one (non-bottom) value. I used the isomorphism (a + b) → c ≅ (a → c) × (b → c), which corresponds to a familiar law of exponents: ca + b = ca × cb.

So the sought domain type q is any type isomorphic to 1 + ⋯ + 1, which is to say a type consisting of exactly n choices.

We have already seen a candidate for the index type q, of which Vec n is the natural trie functor. The post Type-bounded numbers defines a type BNat n corresponding to natural numbers less than n, where n is a type-encoded natural number.

data BNat  ** where
BZero BNat (S n)
BSucc BNat n → BNat (S n)

These two constructors correspond to two axioms about inequality: 0 < n + 1 and m < n ⇒ m + 1 < n + 1. The type BNat n then corresponds to canonoical proofs that m < n for various values of m, where the proofs are built out of the two axioms and the law of modus ponens (which corresponds to function application).

Assuming a type n is built up solely from Z and S, a simple inductive argument shows that the number of fully-defined elements (not containing ) of BNat n is the natural number corresponding to n (i.e., nat ∷ Nat n, where nat is as in the post Doing more with length-typed vectors).

Vectors as numbers

We've seen that Vec is a trie for bounded unary numbers, i.e., BNat n ↛ a ≡ Vec n a, using the notation from Elegant memoization with higher-order types. (Note that I've changed my pretty-printing from "k :→: v" to "k ↛ v".)

It's also the case that a vector of digits can be used to represent numbers:

type Digits n b = Vec n (BNat b)  -- n-digit number in base b

Or, more pleasing to my eye,

type Digits n b = BNat n ↛ BNat b

These representations can be given a little-endian or big-endian interpretation:

littleEndianToZ, bigEndianToZ  ∀ n b. IsNat b ⇒ Digits n b → Integer
littleEndianToZ = foldr' (λ x s → fromBNat x + b * s) 0
where b = natToZ (nat Nat b)
bigEndianToZ    = foldl' (λ s x → fromBNat x + b * s) 0
where b = natToZ (nat Nat b)

The foldl' and foldr' are from Data.Foldable.

Give it a try:

*Vec> let ds = map toBNat [3,5,7]  [BNat TenT]
*Vec> let v3 = fromList ds Vec ThreeT (BNat TenT)
*Vec> v3
fromList [3,5,7]
*Vec> littleEndianToZ v3
753
*Vec> bigEndianToZ v3
357

It's a shame here to map to the unconstrained Integer type, since (a) the result must be a natural number, and (b) the result is statically bounded by bn.

One Comment

  1. Conal Elliott » Blog Archive » A trie for length-typed vectors:

    [...] About « Reverse-engineering length-typed vectors [...]

Leave a comment