# Exercise 3.42 (a) Define takeL, dropL ∷ Nat → List α → List α as a list unfold and natural fold, respectively. First, takeL. The usual definition is takeL Zero xs = Nil takeL (Succ n) Nil = Nil takeL (Succ n) (Cons x xs) = Cons x (takeL n xs) To write this as an unfold, we need access to both the List and Nat arguments. We define an uncurried version of takeL, which gives us the type of our unfold: takeLu ∷ (Nat, List α) → List α ((Nat, List α) → Bool) → ((Nat, List α) → α) → ((Nat, List α) → (Nat, List α)) → (Nat, List α) → List α Using the universal property of unfoldL, takeLu = unfoldL p f g iff takeLu b = if p b then Nil else Cons (f b) (takeLu (g b)) We calculate by case analysis on b ∷ (Nat, List α). Since takeLu (n, xs) is Nil when (1) n = Zero or (2) xs = Nil, we immediately define p (n, xs) = isZero n || nil xs We now consider the case (Succ n, Cons x xs): takeLu (Succ n, Cons x xs) = if p (Succ n, Cons x xs) then Nil else Cons (f (Succ n, Cons x xs)) (takeLu (g (Succ n, Cons x xs))) ≡ { takeLu.3, p def., ITE } Cons x (takeLu (n, xs)) = Cons (f (Succ n, Cons x xs)) (takeLu (g (Succ n, Cons x xs))) We extract the equations for f and g, which are basically the definitions we’re looking for: f (Succ n, Cons x xs) = x g (Succ n, Cons x xs) = (n, xs) The full definition is then takeL = curry takeLu takeLu = unfoldL p f g where p (n, xs) = isZero n || nil xs f (n, Cons x xs) = x g (Succ n, Cons x xs) = (n, xs) * * * Here’s the usual def. of dropL: dropL Zero xs = xs dropL (Succ n) Nil = Nil dropL (Succ n) (Cons x xs) = dropL n xs Using the universal property of foldN: dropL = foldN z s iff dropL n = case n of Zero → z Succ m → s (h m) We have the types: dropL n, foldN z s n ∷ List α → List α z ∷ List α → List α s ∷ (List α → List α) → (List α → List α) We include the argument list xs. Case n = Zero: (foldN z s Zero) xs = dropL Zero xs ≡ { dropL.1 } (foldN z s Zero) xs = xs ≡ { foldN.1 } z xs = xs We define z = id. For the case (Succ n), let’s ignore the “short list” case for a minute. (foldN z s (Succ n)) (Cons x xs) = dropL (Succ n) (Cons x xs) ≡ { foldN.2, dropL.3 } (s (foldN z s n)) (Cons x xs) = dropL n xs ≡ { tail.1 } (s (foldN z s n)) (Cons x xs) = dropL n (tail (Cons x xs)) ≡ { hypothesis } (s (foldN z s n)) (Cons x xs) = (foldN z s n) (tail (Cons x xs)) ≡ { generalize (foldN z s n) to f, rewrite as composition } (s f) (Cons x xs) = (f ∘ tail) (Cons x xs) Now, assume the input list is Nil. (foldN z s (Succ n)) Nil = dropL (Succ n) Nil ≡ { foldN.2, dropL.2 } (s (foldN z s n)) Nil = Nil ≡ { hypothesis, dropL.1 & 2 } (s (dropL n)) Nil = dropL n Nil ≡ { generalize (dropL n) to f } (s f) Nil = f Nil ≡ { id/∘ right identity } (s f) Nil = (f ∘ id) Nil So we have the equations (s f) Nil = (f ∘ id) Nil (s f) (Cons x xs) = (f ∘ tail) (Cons x xs) Rewriting s as (λg → g ∘ h), we replace these with (f ∘ h) Nil = (f ∘ id) Nil (f ∘ h) (Cons x xs) = (f ∘ tail) (Cons x xs) We can see that s is a total version of ‘tail’: s = ttail ttail Nil = Nil ttail (Cons x xs) = xs So our final definition is dropL n = foldN id (λf → ttail ∘ f) n This completes the synthesis. (b) Define unravel: unravel ∷ Nat → List α → List α Gibbons is pretty vague about this function, but it’s an inverse to ravel; ‘unravel h’ splits a list into the subsequences composed of every hth element of the list. We need a “pre-inverse” to concat: sublists ∷ Nat → List α → List (List α) sublists n = unfoldL nil (takeL n) (dropL n) And then we have unravel n = trans ∘ sublists n