The type of a function may encode
a theorem
•
The function map
preserves the length of
lists
map :: (a -> b) -> (List a n) -> (List b n)
map f Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)