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 , cons' represents length , 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.

Articles by others on the same topic (0)

There are currently no matching articles.