Okasaki's PFDS, Chapter 4

This post contains my solutions to the exercises in chapter 4 of Okasaki’s “Purely Functional Data Structures”. The latest source code can be found in my GitHub repo.

Notation

Okasaki uses $ to indicate suspensions. But beware! Haskell also has this symbol but it means something completely different, namely function application. In symbols:

($) :: (a -> b) -> a -> b
($) f a = f a

We can use it like any other function in haskell. For example:

two = (1 +) $ 1

It has nothing to do with suspensions, evaluation, forcing, etc.

It is also important to note that a ‘list’ in haskell is not what Okasaki calls a ‘list’. He would call haskell’s lists ‘streams’. We will stick with haskell’s notation, calling Okasaki’s list a ‘strict list’.

Exercise 1

Show that both definitions of drop are equivalent.

Solution 1

The code in this solution is NOT Haskell.

For convenience, we give names to the three different functions.

fun drop (0, s)            = s
  | drop (n, $Nil)         = $Nil
  | drop (n, $Cons (x, s)) = drop (n-1, s)

fun lazy dropA (0, s)            = s
       | dropA (n, $Nil)         = $Nil
       | dropA (n, $Cons (x, s)) = dropA (n-1, s)

fun lazy dropB (n, s) = drop (n, s)

The proof proceeds in three steps.

Lemma

Let s be a suspension. Then $force s is equivalent to s.

Proof. Suppose s is $e for some expression e. Then $force s ≅ $force $e ≅ $e ≅ s.

□

Lemma

dropA is equivalent to drop

Proof. We prove this by induction on n.

For the base step, dropA (0, s) = $force s $`s = drop (0, s), where the middle equivalence follows by the previous lemma.

Note that dropA (n, $Nil) = $force $Nil = $Nil = drop (n, $Nil) follows by the previous lemma. Now suppose dropA (n, s) ≅ drop (n, s) for some n∈N and any stream s. We can write s as $Cons (x, s'). Then dropA (n+1, s) = dropA (n+1, $Cons (x, s')) = $force dropA (n, s') ≅ dropA (n, s') ≅ drop (n, s') = drop (n+1, s).

□

Lemma

dropA is equivalent to dropB

Proof. Using the previous two lemmas, we obtain dropB (n, s) = $force drop (n, s) = $force dropA (n, s) = dropA (n, s) for any n∈N and any stream s.

□

Exercise 2

Implement insertion sort on streams and show that extracting the first k elements takes only O(nk) time, where n is the length of the input list.

Solution 2

See source. Note that lists in Haskell are what Okasaki calls streams, so we need no special annotations or data structures.

Let T(n,k) be the asymptotic complexity of computing take k $ sort xs, where xs is a list of length n. By definition of take, T(n,0)=O(1) and T(0,k)=T(0,0).

In take k $ sort xs the function take k needs to put sort xs into weak head normal form. Let S(m) be the complexity of puting sort ys into weak head normal form for a list ys of length m. Clearly S(0)=O(1). Since sort (y:ys) = ins y $ sort ys, we have S(m)=S(m−1)+O(1), since ins y only needs to put sort ys into weak head normal form. This is solved by S(m)=O(m).

Now, take k $ sort xs = take k $ y : ys = y : take (k-1) ys, where sort xs = y : ys. Thus T(n,k)=T(n−1,k−1)+O(n). This recurrence is solved by T(n,k)=O(nk).