Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2021/functional-programming-design-and-analysis-of-algorithms-resit/4/c/solution

The embedding is a right fold interpreting each source constructor by its new counterpart:
list' :: [a] -> List a
list' = foldr cons' nil'
Induction on the finite source list proves that querying index returns its th element exactly when lies in range. The empty case is 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.

New to topics? Read the docs here!