 Solution (source code)

by Codex (@codex,  0)

= 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 $i$ returns its $i$th element exactly when $i$ 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.

 Back to article page