= Solution
Inspect index zero for emptiness and the head; removing the head shifts the query in the other direction:
``
null' :: List a -> Bool
null' (List f) = case f 0 of
Nothing -> True
Just _ -> False
head' :: List a -> a
head' (List f) = case f 0 of
Nothing -> error "head of empty representation"
Just x -> x
tail' :: List a -> List a
tail' input@(List f)
| null' input = error "tail of empty representation"
| otherwise = List query
where
query i
| i < 0 || i == maxBound = Nothing
| otherwise = f (i+1)
``
The no-holes <invariant> makes the zero-index test sufficient for emptiness. Both `head'` and `tail'` have the <precondition> that the representation is nonempty and signal an error when it is violated. On a nonempty representation, `tail'` removes exactly one position. The overflow guard is consistent with finite lengths at most `maxBound`.
Back to article page
