loop
Lets start with a case study that is simple enough to explain without pages of code, yet complex enough to show off whats cool about dependency: Chris Okasaki’s beautiful Lazy Queues. This structure leans heavily on an invariant to provide fast insertion and deletion. Let’s see how to enforce that invariant with LiquidHaskell.
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.
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.
insert
elements, we just cons them onto the back
list,remove
elements, we just un-cons them from the front
list.
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:
remove
call is triggered, andfront
list is empty.
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:
A type for List
s, and a way to track their size
,
A type for Queue
s which encodes the balance invariant
A way to implement the insert
, remove
and transfer
operations.
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
:
Exercise: (Destructing Lists): We can destruct lists by writing a hd
and tl
function as shown below. Fix the specification or implementation such that the definitions typecheck.
Hint: When you are done, okHd
should be verified, but badHd
should be rejected.
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:
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 Queue
s, which together with the key balance invariant, ensures that the calls to hd
and tl
are safe.
Exercise: (Whither pattern matching?): Can you explain why we (or Okasaki) didn’t use pattern matching here, and have instead opted for the explicit hd
and tl
?
Exercise: (Queue Sizes): If you did the List Destructing exercise above, then you will notice that the code for remove
has a type error: namely, the calls to hd
and tl
may fail if the f
list is empty.
QueueN
below, andremove
a type that verifies the safety of the calls made to hd
and tl
.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:
Exercise: (Insert): Write down a type for insert
such that replicate
and okReplicate
are accepted by LiquidHaskell, but badReplicate
is rejected.
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.
Exercise: (Rotate): The Rotate function rot
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. Write down a type for rot
so that it typechecks and verifies the type for makeq
.
Hint: You may have to modify a precondition in makeq
to capture the relationship between f
and b
.
Exercise: (Transfer): Write down a signature for take
which extracts n
elements from its input q
and puts them into a new output Queue. When you are done, okTake
should be accepted, but badTake
should be rejected.
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
size
to guarantee the invariants, and