The empty representation is nowhere present; prepending shifts all old positions by one:For a represented length ,
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)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
There are currently no matching articles.