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
Vec n a isomorphic to
q → a (for all
Turning this question on its head, what simpler type gives rise to length-typed vectors in a standard fashion?
- 2011-02-01: Define
Digits n bas
BNat n ↛ BNat b.
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 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
S, a simple inductive argument shows that the number of fully-defined elements (not containing
BNat n is the natural number corresponding to
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)
foldr' are from
Give it a try:
*Vec> let ds = map toBNat [3,5,7] ∷ [BNat TenT]
*Vec> let v3 = fromList ds ∷ Vec ThreeT (BNat TenT)
*Vec> littleEndianToZ v3
*Vec> bigEndianToZ v3
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.