# 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`

\(\cong\) `$force $e`

\(\cong\) `$e`

\(\cong\) `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)`

\(\cong\) `drop (n, s)`

for some \(n \in \mathbb 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')`

\(\cong\) `dropA (n, s')`

\(\cong\) `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 \in \mathbb N\) and any stream `s`

.

□

## Exercise 2

Implement insertion sort on streams and show that extracting the first \(k\) elements takes only \(\mathcal 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) = \mathcal 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) = \mathcal O (1)\). Since `sort (y:ys) = ins y $ sort ys`

, we have \(S (m) = S (m-1) + \mathcal O (1)\), since `ins y`

only needs to put `sort ys`

into weak head normal form. This is solved by \(S (m) = \mathcal 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) + \mathcal O (n)\). This recurrence is solved by \(T (n, k) = \mathcal O (nk)\).