= Solution
The empty representation is nowhere present; prepending shifts all old positions by one:
``
nil' :: List a
nil' = List (\_ -> Nothing)
cons' :: a -> List a -> List a
cons' x (List f) = List query
where
query i
| i < 0 = Nothing
| i == 0 = Just x
| otherwise = f (i-1)
``
For a represented length $m$, `cons'` represents length $m+1$, provided that length is representable. Index zero is the new head and each later valid index asks for the preceding old position. The no-holes <invariant> is preserved. No conventional <list> is built by either constructor.
Back to article page
