## 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: *c*^{a + b} = *c*^{a} × *c*^{b}.

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 *b*^{n}.

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

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

31 January 2011, 3:04 pm