How to use length annotated lists in Haskell

Question

Apparently, with some GHC extensions it is possible to define a type of list that has length encoded in the type, like this:

{-# LANGUAGE GADTs, EmptyDataDecls #-}

data Z
data S a

data List l a where
  Nil  :: List Z a
  Cons :: a -> List l a -> List (S l) a

While I see why this can be useful, I have trouble actually using it.

How can one create such a list? (Apart from hardcoding it into the program.)

Say one would want to create a program that reads two such lists from terminal and computes their dot product. While it is easy to implement the actual multiplicative function, how can the program read the data?

Could you point me to some existing code that uses these techniques?

Answer 1

You don't have to hard-code the length of the list; instead, you can define the following type:

data UList a where
    UList :: Nat n => List n a -> UList a

where

class Nat n where
    asInt :: n -> Int

instance Nat Z where
    asInt _ = 0

instance Nat n => Nat (S n) where
    asInt x = 1 + asInt (pred x)
      where
        pred = undefined :: S n -> n

and we also have

fromList :: [a] -> UList a
fromList [] = UList Nil
fromList (x:rest) =
    case fromList rest of
        UList xs -> UList (Cons x xs)

This setup allows you to create lists whose lengths are not known at compile time; you can access the length by doing a case pattern match to extract the type from the existential wrapper, and then use the Nat class to turn the type into an integer.

You might wonder what the advantage is of having a type that you don't know the value of at compile time; the answer is that although you don't know what the type will be, you can still enforce invariants. For example, the following code is guaranteed to not change the length of the list:

mapList :: (a -> b) -> List n a -> List n b

And if we have type addition using a type family called, say, Add, then we can write

concatList :: List m a -> List n a -> List (Add m n) a

which enforces the invariant that concatenating two lists gets you a new list with the sum of the two lengths.