Case Study: Okasaki’s Lazy Queues

Queues

A queue is a structure into which we can insert and remove data such that the order in which the data is removed is the same as the order in which it was inserted.

Figure 1.1: A Queue is a structure into which we can insert and remove elements. The order in which the elements are removed is the same as the order in which they were inserted.

To efficiently implement a queue we need to have rapid access to both the front as well as the back because we remove elements from former and insert elements into the latter. This is quite straightforward with explicit pointers and mutation – one uses an old school linked list and maintains pointers to the head and the tail. But can we implement the structure efficiently without having stoop so low?

Chris Okasaki came up with a very cunning way to implement queues using a pair of lists – let’s call them front and back which represent the corresponding parts of the Queue.

• To insert elements, we just cons them onto the back list,
• To remove elements, we just un-cons them from the front list.

Figure 1.2: We can implement a Queue with a pair of lists; respectively representing the front and back.

The catch is that we need to shunt elements from the back to the front every so often, e.g. we can transfer the elements from the back to the front, when:

1. a remove call is triggered, and
2. the front list is empty.

Figure 1.3: Transferring Elements from back to front.

Okasaki's first insight was to note that every element is only moved once from the back to the front; hence, the time for insert and remove could be O(1) when amortized over all the operations. This is perfect, except that some set of unlucky remove calls (which occur when the front is empty) are stuck paying the bill. They have a rather high latency up to O(n) where n is the total number of operations.

Okasaki's second insight saves the day: he observed that all we need to do is to enforce a simple balance invariant:

\[\mbox{Size of front} \geq \mbox{Size of back}\]

If the lists are lazy i.e. only constructed as the head value is demanded, then a single remove needs only a tiny O(log n) in the worst case, and so no single remove is stuck paying the bill.

Lets implement Queues and ensure the crucial invariant(s) with LiquidHaskell. What we need are the following ingredients:

1. A type for Lists, and a way to track their size,

2. A type for Queues which encodes the balance invariant

3. A way to implement the insert, remove and transfer operations.

Sized Lists

The first part is super easy. Let’s define a type:

We have a special field that saves the size because otherwise, we have a linear time computation that wrecks Okasaki’s careful analysis. (Actually, he presents a variant which does not require saving the size as well, but that’s for another day.)

How can we be sure that size is indeed the real size of elems? Let’s write a function to measure the real size:

Now, we can simply specify a refined type for SList that ensures that the real size is saved in the size field:

As a sanity check, consider this:

Lets define an alias for lists of a given size N:

Finally, we can define a basic API for SList.

To Construct lists, we use nil and cons:

Hint: When you are done, okHd should be verified, but badHd should be rejected.

Queue Type

It is quite straightforward to define the Queue type, as a pair of lists, front and back, such that the latter is always smaller than the former:

The alias SListLE a L corresponds to lists with at most N elements:

As a quick check, notice that we cannot represent illegal Queues:

Queue Operations

Almost there! Now all that remains is to define the Queue API. The code below is more or less identical to Okasaki’s (I prefer front and back to his left and right.)

The Empty Queue is simply one where both front and back are both empty:

To Remove an element we pop it off the front by using hd and tl. Notice that the remove is only called on non-empty Queues, which together with the key balance invariant, ensures that the calls to hd and tl are safe.

Hint: When you are done, okRemove should be accepted, badRemove should be rejected, and emp should have the type shown below:

To Insert an element we just cons it to the back list, and call the smart constructor makeq to ensure that the balance invariant holds:

To Ensure the Invariant we use the smart constructor makeq, which is where the heavy lifting happens. The constructor takes two lists, the front f and back b and if they are balanced, directly returns the Queue, and otherwise transfers the elements from b over using the rotate function rot described next.

Hint: You may have to modify a precondition in makeq to capture the relationship between f and b.

Recap

Well there you have it; Okasaki’s beautiful lazy Queue, with the invariants easily expressed and checked with LiquidHaskell. This example is particularly interesting because

1. The refinements express invariants that are critical for efficiency,
2. The code introspects on the size to guarantee the invariants, and
3. The code is quite simple and we hope, easy to follow!