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.