Conal Elliott

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