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> v3fromList [3,5,7]*Vec> littleEndianToZ v3753*Vec> bigEndianToZ v3357``

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 […]