A function returning an optional value supplies the representation:For a finite represented list, require a length such that every index returns
newtype List a = List (Int -> Maybe a)Just its element and every other index returns Nothing. Thus there are no holes: absence at a nonnegative index implies absence at every later index. The type alone does not enforce this invariant, or algorithm termination of a query. An infinite represented sequence may instead have a present value at every nonnegative index; operations requiring its length will not terminate.The implementations below return
Nothing at negative indices. Finite lengths, requested counts and intermediate indices are assumed to fit Int; explicit guards on index shifts also prevent arithmetic wraparound from exposing an invalid element.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.The embedding is a right fold interpreting each source constructor by its new counterpart:Induction on the finite source list proves that querying index returns its th element exactly when lies in range. The empty case is
list' :: [a] -> List a
list' = foldr cons' nil'nil'; the cons case shifts every tail index as established in part (b). This is the only part of Question 4 whose implementation uses the conventional list type.Inspect index zero for emptiness and the head; removing the head shifts the query in the other direction:The no-holes invariant makes the zero-index test sufficient for emptiness. Both
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)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.Preserve absence and transform only a present value:Every query keeps its presence status, so the represented length and the no-holes invariant are unchanged. The transformed element is computed only when demanded.
map' :: (a -> b) -> List a -> List b
map' g (List f) = List (\i -> case f i of
Nothing -> Nothing
Just x -> Just (g x))Clamp a nonpositive count to zero. Taking restricts the domain of present indices; dropping translates that domain:For finite length , the first two operations give lengths and , respectively. The length loop reaches the first absent index, namely , so it terminates for a total finite representation. It does not terminate on an infinite represented sequence. There is no assumption that an arbitrary stored query function takes constant time.
take' :: Int -> List a -> List a
take' count (List f) = List query
where
k = max 0 count
query i
| i < 0 || i >= k = Nothing
| otherwise = f i
drop' :: Int -> List a -> List a
drop' count (List f) = List query
where
k = max 0 count
query i
| i < 0 || i > maxBound - k = Nothing
| otherwise = f (i+k)
length' :: List a -> Int
length' (List f) = countFrom 0
where
countFrom i = case f i of
Nothing -> i
Just _ -> countFrom (i+1)Merge by comparing the present heads and consuming just the chosen one. The implementation uses only the functional representation:The two recursive inputs are the disjoint initial and final portions of the represented sequence; they preserve every occurrence and have smaller lengths when . In
merge' :: Ord a => List a -> List a -> List a
merge' left right
| null' left = right
| null' right = left
| head' left <= head' right =
cons' (head' left) (merge' (tail' left) right)
| otherwise =
cons' (head' right) (merge' left (tail' right))
mergeSort' :: Ord a => List a -> List a
mergeSort' input =
let n = length' input
middle = n `div` 2
in if n <= 1 then input
else merge' (mergeSort' (take' middle input))
(mergeSort' (drop' middle input))merge', the smaller current head can precede every remaining value in both sorted inputs. Selecting the left head on equality preserves stability. Each merge step reduces the total number of remaining elements, and induction proves a sorted permutation of the original sequence.This establishes algorithm termination and correctness on total finite representations, not an unconditional implementation bound. Nested index functions can make queries costly, and repeatedly finding lengths or heads may revisit them. The familiar merge-sort bound assumes suitable constant-time access or consumption primitives; the source's function-only representation supplies no such cost guarantee.
Articles by others on the same topic
There are currently no matching articles.