Real-Time Queues

RealTimeQueue.elm

Recall the BankersQueue representation:

-- invariant:
--   frontSize >= backSize
--
type Queue a =
  Q { frontSize : Int         -- frontSize = |front|
    , front : ThunkList a
    , backSize : Int          -- backSize  = |back|
    , back : ThunkList a
    }

Consider the following example from this article; below, append and reverse refer to the lazy list operations:

q_0 = { front = [] , back = [] }

q_1 = enqueue 1 q_0   front_1 = append [] (reverse [1])
q_2 = enqueue 2 q_1
q_3 = enqueue 3 q_2   front_3 = append front_1 (reverse [3,2])
q_4 = enqueue 4 q_3
q_5 = enqueue 5 q_4
q_6 = enqueue 6 q_5
q_7 = enqueue 7 q_6   front_6 = append front_3 (reverse [7,6,5,4])
                              = append (append (append []
                                                       (reverse [1]))
                                               (reverse [3,2]))
                                       (reverse [7,6,5,4])

q_6' = dequeue q_7    -- forces 3-nested append thunks, forces reverse [1]
q_5' = dequeue q_6'   -- forces reverse [3,2]
q_4' = dequeue q_5'
q_3' = dequeue q_4'   -- forces reverse [7,6,5,4]
q_2' = dequeue q_3'
q_1' = dequeue q_2'
q_0' = dequeue q_1'

This demonstrates two situations in which an individual dequeue (or peek) operation may take longer than O(1) amortized time:

  1. O(n) time to reverse, and
  2. O(log n) time to force nested appends.

Step 0

Recall from before that back might as well be a normal List a.

 type Queue a =
   Q { frontSize : Int
     , front : ThunkList a
     , backSize : Int
     , back : List a
     }

Step 1

Combine append and reverse into an incremental function rotate that performs one step of each at a time:

appendFrontRevBack : ThunkList a -> List a -> ThunkList a
appendFrontRevBack front back =
  let
    rotate : ThunkList a -> List a -> ThunkList a -> ThunkList a
    rotate xs ys acc =
      case (force xs, ys) of
        (Nil, y::[]) ->
          lazy (\_ -> Cons y acc)
        (Cons x xs_ , y::ys_) ->
          lazy (\_ -> Cons x (rotate xs_ ys_ (lazy (\_ -> Cons y acc))))
        _ ->
          Debug.todo "rotate should be called with |ys| = |xs| + 1"
  in
  rotate front back (lazy (\() -> Nil))

When rotate is intially called, the arguments will be such that |back| = 1 + |front|.

We can swap this in to check from BankersQueue...

check frontSize front backSize back =
  if frontSize >= backSize then
    Q { frontSize = frontSize, front = front, backSize = backSize, back = back }
  else
    Q { frontSize = frontSize + backSize
      , front = appendFrontRevBack front back
      , backSize = 0
      , back = lazy (\() -> Nil)
      }

... but these thunks will still build up as elements are enqueued without any operations that force the front. So, systematically force the prefix of front.

Step 2

Add a "schedule" ThunkList a that is a suffix of front that has yet to be forced (the prefix has already been forced). The implementation enforces the invariant that the size of sched is equal to the size of front minus the size of back. This invariant obviates the need to maintain Int size information explicitly.

-- invariants:
--    |front| >= |back|
--    |sched|  = |front| - |back|
--
type Queue a =
  Q { front : ThunkList a
    , back : List a
    , sched : ThunkList a
    }

empty : Queue a
empty =
  Q { front = lazy (\() -> Nil)
    , back = []
    , sched = lazy (\() -> Nil)
    }

Because of the invariant, sched is empty when the lengths of front and back are the same. So after either dequeueing from the front or enqueueing to the back, the exec helper function checks whether the schedule is empty. The act of checking forces the schedule.

exec front back sched =
  case force sched of
    Nil ->
      let newFront = appendFrontRevBack front back in
      Q { front = newFront, back = [], sched = newFront }
    Cons _ schedRest ->
      Q { front = front, back = back, sched = schedRest }

enqueue : a -> Queue a -> Queue a
enqueue a (Q {front, back, sched}) =
  exec front (a::back) sched

dequeue : Queue a -> Maybe (Queue a)
dequeue (Q {front, back, sched}) =
  case force front of
    Nil ->
      Nothing
    Cons _ frontRest ->
      Just (exec frontRest back sched)

Scheduling will ensure that that front has already been forced:

peek : Queue a -> Maybe a
peek (Q {front}) =
  case force front of
    Nil -> Nothing
    Cons a _ -> Just a


Reading

Optional