content: 
  Case Study: Okasaki's Lazy Queues {#lazyqueue}
  =================================
  
  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][okasaki95].
  This structure leans heavily on an invariant to provide fast
  *insertion* and *deletion*. Let's see how to enforce that
  invariant with LiquidHaskell.
  
  \begin{comment}
  \begin{code}
  {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--maxparams=3"    @-}
  
  module Tutorial_09_Case_Study_Lazy_Queues 
    (Queue, insert, remove, emp, realSize) 
    where
  
  import Prelude hiding (replicate, take, length)
  
  -- | Size function actually returns the size: (Duh!)
  
  {-@ size :: q:SList a -> {v:Nat | v = size q} @-}
  
  {-@ die :: {v:String | false} -> a @-}
  die x = error x
  
  {-@ invariant {v:SList a | size v >= 0} @-}
  
  -- Source: Okasaki, JFP 1995
  -- http://www.westpoint.edu/eecs/SiteAssets/SitePages/Faculty%20Publication%20Documents/Okasaki/jfp95queue.pdf
  
  replicate :: Int -> a -> Queue a
  
  
  -- {-@ ignore badList @-}
  -- {-@ ignore hd   @-}
  -- {-@ ignore tl   @-}
  -- {-@ ignore badQ @-}
  
  \end{code}
  \end{comment}
  
  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.
  
  <div class="figure"
    id="fig:queue"
    caption="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."
    height="200px"
    file="img/queue.png">
  </div>
  
  \newthought{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?
  
  \newthought{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.
  
  <div class="figure"
       id="fig:queue-pair"
       height="200px"
       file="img/queue-lists.png"
       caption="We can implement a Queue with a pair of lists;
                respectively representing the front and back.">
  </div>
  
  \newthought{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.
  
  <div class="figure"
       id="fig:queue-transfer"
       height="200px"
       file="img/queue-rotate.png"
       caption="Transferring Elements from back to front.">
  </div>
  
  \newthought{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.
  
  \newthought{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}$$
  
  \noindent 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.
  
  
  \newthought{Lets implement 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
  
  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.)
  
  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}
  
  
  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}
  
  \newthought{Lets define an alias} for lists of a given size `N`:
  
  \begin{code}
  {-@ type SListN a N = {v:SList a | size v = N} @-}
  \end{code}
  
  \noindent
  Finally, we can define a basic API for `SList`.
  
  \newthought{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}
  
  <div class="hwex" id="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.
  </div>
  
  \begin{code}
  {-@ tl           :: xs:SList a -> SListN a {size xs - 1}  @-}
  tl (SL n (_:xs)) = SL (n-1) xs
  tl _             = die "empty SList"
  
  {-@ hd           :: xs:SList a -> a @-}
  hd (SL _ (x:_))  = x
  hd _             = die "empty SList"
  \end{code}
  
  \hint When you are done, `okHd` should be verified, but `badHd` should be rejected.
  
  \begin{code}
  {-@ okList :: SListN String 1 @-}
  
  okHd  = hd okList       -- accepted
  
  badHd = hd (tl okList)  -- rejected
  \end{code}
  
  
  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:
  
  \begin{code}
  {-@ data Queue a = Q {
        front :: SList a
      , back  :: SListLE a (size front)
      }
  @-}
  data Queue a = Q
    { front :: SList a
    , back  :: SList a
    }
  \end{code}
  
  \newthought{The alias} `SListLE a L` corresponds to lists with at most `N` elements:
  
  \begin{code}
  {-@ type SListLE a N = {v:SList a | size v <= N} @-}
  \end{code}
  
  \noindent
  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}
  
  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`.)
  
  \newthought{The Empty Queue} is simply one where both `front` and
  `back` are both empty:
  
  \begin{code}
  emp = Q nil nil
  \end{code}
  
  \newthought{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 f b)   = (hd f, makeq (tl f) b)
  \end{code}
  
  <div class="hwex" id="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`?
  </div>
  
  <div class="hwex" id="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.
  
  1. Write a *measure* to describe the queue size,
  2. Use it to complete the definition of `QueueN` below, and
  3. Use it to give `remove` a type that verifies the safety of the
     calls made to `hd` and `tl`.
  </div>
  
  \hint When you are done, `okRemove` should be accepted, `badRemove`
  should be rejected, and `emp` should have the type shown below:
  
  
  \begin{code}
  -- | Queues of size `N`
  {-@ type QueueN a N = {v:Queue a | true} @-}
  
  okRemove  = remove example2Q   -- accept
  badRemove = remove example0Q   -- reject
  
  {-@ emp :: QueueN _ 0 @-}
  
  {-@ example2Q :: QueueN _ 2 @-}
  example2Q = Q (1 `cons` (2 `cons` nil)) nil
  
  {-@ example0Q :: QueueN _ 0 @-}
  example0Q = Q nil nil
  \end{code}
  
  
  
  \newthought{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 e (Q f b) = makeq f (e `cons` b)
  \end{code}
  
  <div class="hwex" id="Insert">Write down a type for `insert` such
  that `replicate` and `okReplicate` are accepted by LiquidHaskell, but `badReplicate`
  is rejected.
  </div>
  
  \begin{code}
  {-@ replicate :: n:Nat -> a -> QueueN a n @-}
  replicate 0 _ = emp
  replicate n x = insert x (replicate (n-1) x)
  
  {-@ okReplicate :: QueueN _ 3 @-}
  okReplicate = replicate 3 "Yeah!"  -- accept
  
  {-@ badReplicate :: QueueN _ 3 @-}
  badReplicate = replicate 1 "No!"   -- reject
  \end{code}
  
  
  \newthought{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.
  
  \begin{code}
  {-@ makeq :: f:SList a -> b:SList a -> QueueN a {size f + size b} @-}
  makeq f b
    | size b <= size f = Q f b
    | otherwise        = Q (rot f b nil) nil
  \end{code}
  
  <div class="hwex" id="Rotate"> \doublestar
  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`.
  </div>
  
  \hint You may have to modify a precondition in `makeq` to capture the
  relationship between `f` and `b`.
  
  \begin{code}
  rot f b acc
    | size f == 0 = hd b `cons` acc
    | otherwise   = hd f `cons` rot (tl f) (tl b) (hd b `cons` acc)
  \end{code}
  
  
  <div class="hwex" id="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.
  </div>
  
  \begin{code}
  take           :: Int -> Queue a -> (Queue a, Queue a)
  take 0 q       = (emp          , q)
  take n q       = (insert x out , q'')
    where
      (x  , q')  = remove q
      (out, q'') = take (n-1) q'
  
  {-@ okTake :: (QueueN _ 2, QueueN _ 1) @-}
  okTake   = take 2 exampleQ  -- accept
  
  badTake  = take 10 exampleQ -- reject
  
  exampleQ = insert "nal" $ insert "bob" $ insert "alice" $ emp
  \end{code}
  
  
  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!
  