Conal Elliott

Fixing lists

Is there a type of finite lists without choice points (sums)? Yes. There are lots of them. One for each length. Instead of having a single type of lists, have an infinite family of types of n-element lists, one type for each n.

In other words, to fix the problem with lists (trie-unfriendliness), split up the usual list type into subtypes (so to speak), each of which has a fixed length.

I realize I'm changing the question to a simpler one. I hope you'll forgive me and hang in to see where this ride goes.

As a first try, we might use tuples as our fixed-length lists:

type L0 a = ()
type L1 a = (a)
type L2 a = (a,a)
type L3 a = (a,a,a)
⋯

However, we can only write down finitely many such types, and I don't know how we could write any definitions that are polymorphic over length.

What can "polymorphic over length" mean in a setting like Haskell, where polymorphism is over types rather than values. Can we express numbers (for lengths, etc) as types? Yes, as in the previous post, Type-bounded numbers, using a common encoding:

data Z    -- zero
data S n  -- successor

Given these type-level numbers, we can define a data type Vec n a, containing only vectors (fixed lists) of length n and elements of type a. Such vectors can be built up as either the zero-length vector, or by adding an element to an vector of length n to get a vector of length n + 1. I don't know how to define this type as a regular algebraic data type, but it's easy as a generalized algebraic data type (GADT):

infixr 5 :<

data Vec ∷ * → * → * where
  ZVec ∷                Vec Z     a
  (:<) ∷ a → Vec n a → Vec (S n) a

For example,

*Vec> :ty 'z' :< 'o' :< 'm' :< 'g' :< ZVec
'z' :< 'o' :< 'm' :< 'g' :< ZVec ∷ Vec (S (S (S (S Z)))) Char

As desired, Vec is length-typed, covers all (finite) lengths, and allows definition of length-polymorphic functions. For instance, it's easy to map functions over vectors:

instance Functor (Vec n) where
  fmap _ ZVec     = ZVec
  fmap f (a :< u) = f a :< fmap f u

The type of fmap here is (a → b) → Vec n a → Vec n b.

Folding over vectors is also straightforward:

instance Foldable (Vec n) where
  foldr _ b ZVec      = b
  foldr h b (a :< as) = a `h` foldr h b as

Is Vec n an applicative functor as well?

instance Applicative (Vec n) where
  ⋯

We would need

pure ∷ a → Vec n a
(⊛)  ∷ Vec n (a → b) → Vec n a → Vec n b

The (⊛) method can be defined similarly to fmap:

  ZVec      ⊛ ZVec      = ZVec
  (f :< fs) ⊛ (x :< xs) = f x :< (fs ⊛ xs)

Unlike fmap and (⊛), pure doesn't have a vector structure to crawl over. It must create just the right structure anyway. You might enjoy thinking about how to solve this puzzle, which I'll tackle in my next post. (Warning: spoilers in the comments below.)