---
layout: post
title: "Okasaki's Lazy Queues"
date: 2015-01-28
comments: true
external-url:
author: Ranjit Jhala 
published: true
categories: measures
demo: LazyQueue.hs
---

The "Hello World!" example for fancy type systems is probably the sized vector
or list `append` function ("The output has size equal to the *sum* of the
inputs!").  One the one hand, it is perfect: simple enough to explain without
pages of code, yet complex enough to show off whats cool about dependency. On
the other hand, like the sweater I'm sporting right now, it's a bit well-worn and
worse, was never wholly convincing ("Why do I *care* what the *size* of the
output list is anyway?")

Recently, I came across a nice example that is almost as simple, but is also
well motivated: Okasaki's beautiful [Lazy Amortized Queues][okasaki95].  This
structure leans heavily on an invariant to provide fast *insertion* and
*deletion*. Let's see how to enforce that invariant with LiquidHaskell.

<!-- more -->

<div class="hidden">
\begin{code}
{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--total"          @-}
{-@ LIQUID "--maxparams=3"    @-}

module LazyQueue (Queue, insert, remove, emp) where

import Prelude hiding (length)

-- | Size function actually returns the size: (Duh!)

{-@ size :: q:SList a -> {v:Nat | v = size q} @-}
data Queue a = Q  { front :: SList a
                  , back  :: SList a
                  }

-- Source: Okasaki, JFP 1995
-- http://www.westpoint.edu/eecs/SiteAssets/SitePages/Faculty%20Publication%20Documents/Okasaki/jfp95queue.pdf

\end{code}
</div>

Queues 
------

A [queue][queue-wiki] 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.

![A Queue](/images/queue.png)

To implement a queue *efficiently* one needs to have rapid access to both
the "head" as well as the "tail" 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?

Queues = Pair of Lists
----------------------

Almost two decades ago, 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.

![A Queue is Two Lists](/images/queue-lists.png)


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

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

We can transfer the elements from the `back` to the `front`.


![Transferring Elements from Back to Front](/images/queue-rotate.png)

Okasaki observed that every element is only moved *once* from the
front to the back; hence, the time for `insert` and `lookup` could be
`O(1)` when *amortized* over all the operations. Awesome, right?!

Almost. 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. Oops.

Queue = Balanced Lazy Lists
---------------------------

This is where Okasaki's beautiful insights kick in. Okasaki
observed that all we need to do is to enforce a simple invariant:

**Invariant:** Size of `front` >= Size of `back`

Now, 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.

Let's see how to represent these Queues and ensure the crucial invariant(s)
with LiquidHaskell. What we need are the following ingredients:

1. A type for `List`s, and a way to track their `size`,

2. A type for `Queue`s which encodes the *balance* invariant -- ``front longer than back",

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

Sized Lists
------------

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

\begin{code}
data SList a = SL { size :: Int, elems :: [a]}
\end{code}

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.)

But how can we be sure that `size` is indeed the *real size* of `elems`?

Let's write a function to *measure* the real size:

\begin{code}
{-@ measure realSize @-}
realSize      :: [a] -> Int
realSize []     = 0
realSize (_:xs) = 1 + realSize xs
\end{code}

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

\begin{code}
{-@ data SList a = SL {
       size  :: Nat 
     , elems :: {v:[a] | realSize v = size}
     }
  @-}
\end{code}

As a sanity check, consider this:

\begin{code}
okList  = SL 1 ["cat"]    -- accepted

badList = SL 1 []         -- rejected
\end{code}

It is helpful to define a few aliases for `SList`s of a size `N` and
non-empty `SList`s:

\begin{code}
-- | SList of size N

{-@ type SListN a N = {v:SList a | size v = N} @-}

-- | Non-Empty SLists:

{-@ type NEList a = {v:SList a | size v > 0} @-}

\end{code}

Finally, we can define a basic API for `SList`.

**To Construct** lists, we use `nil` and `cons`:

\begin{code}
{-@ nil          :: SListN a 0  @-}
nil              = SL 0 []

{-@ cons         :: a -> xs:SList a -> SListN a {size xs + 1}   @-}
cons x (SL n xs) = SL (n+1) (x:xs)
\end{code}

**To Destruct** lists, we have `hd` and `tl`.

\begin{code}
{-@ tl           :: xs:NEList a -> SListN a {size xs - 1}  @-}
tl (SL n (_:xs)) = SL (n-1) xs

{-@ hd           :: xs:NEList a -> a @-}
hd (SL _ (x:_))  = x 
\end{code}

Don't worry, they are perfectly *safe* as LiquidHaskell will make
sure we *only* call these operators on non-empty `SList`s. For example,

\begin{code}
okHd  = hd okList       -- accepted

badHd = hd (tl okList)  -- rejected
\end{code}


Queue Type
-----------

Now, 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:

\begin{code}
{-@ data Queue a = Q {
       front :: SList a 
     , back  :: SListLE a (size front)
     }
  @-}
\end{code}

Where the alias `SListLE a L` corresponds to lists with less than `N` elements:

\begin{code}
{-@ type SListLE a N = {v:SList a | size v <= N} @-}
\end{code}

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

\begin{code}
okQ  = Q okList nil  -- accepted, |front| > |back| 

badQ = Q nil okList  -- rejected, |front| < |back|
\end{code}

**To Measure Queue Size** let us define a function

\begin{code}
{-@ measure qsize @-}
qsize         :: Queue a -> Int
qsize (Q l r) = size l + size r
\end{code}

This will prove helpful to define `Queue`s of a given size `N` and
non-empty `Queue`s (from which values can be safely removed.)

\begin{code}
{-@ type QueueN a N = {v:Queue a | N = qsize v} @-}
{-@ type NEQueue a  = {v:Queue a | 0 < qsize v} @-}
\end{code}


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 `nil`.

\begin{code}
{-@ emp :: QueueN a 0 @-}
emp = Q nil nil
\end{code}

**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:

\begin{code}
{-@ insert       :: a -> q:Queue a -> QueueN a {qsize q + 1}   @-}
insert e (Q f b) = makeq f (e `cons` b)
\end{code}

**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 `Queue`s, which together
with the key balance invariant, ensures that the calls to `hd` and `tl` are safe.

\begin{code}
{-@ remove       :: q:NEQueue a -> (a, QueueN a {qsize q - 1}) @-}
remove (Q f b)   = (hd f, makeq (tl f) b)
\end{code}

*Aside:* Why didn't we (or Okasaki) use a pattern match here?

**To Ensure the Invariant** we use the smart constructor `makeq`,
which is where the heavy lifting, such as it is, 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 `rot`ate.

\begin{code}
{-@ makeq :: f:SList a
          -> b:SListLE a {size f + 1 }
          -> QueueN a {size f + size b}
  @-}
makeq l r
  | size r <= size l = Q l r
  | otherwise        = Q (rot l r nil) nil
\end{code}

**The Rotate** function is only called when the `back` is one larger
than the `front` (we never let things drift beyond that). It is
arranged so that it the `hd` is built up fast, before the entire
computation finishes; which, combined with laziness provides the
efficient worst-case guarantee.

\begin{code}
{-@ rot :: l:SList a
        -> r:SListN _ {1 + size l}
        -> a:SList _
        -> SListN _ {size l + size r + size a}
  @-}
rot l r a
  | size l == 0 = hd r `cons` a
  | otherwise   = hd l `cons` rot (tl l) (tl r) (hd r `cons` a)
\end{code}

Conclusion
----------

Well there you have it; Okasaki's beautiful lazy Queue, with the
invariants easily expressed and checked with LiquidHaskell. I find
this example particularly interesting because the refinements express
invariants that are critical for efficiency, and furthermore the code
introspects on the `size` in order to guarantee the invariants.  Plus,
it's just marginally more complicated than `append` and so, (I hope!)
was easy to follow.



[okasaki95]: http://www.westpoint.edu/eecs/SiteAssets/SitePages/Faculty%20Publication%20Documents/Okasaki/jfp95queue.pdf

[queue-wiki]: http://en.wikipedia.org/wiki/Queue_%28abstract_data_type%29