Functional queue

A singly linked list gives constant-time access to one end only, so a queue, which adds at one end and removes at the other, cannot be a single immutable list. A functional queue uses two: a front list, whose head is the next element to leave, and a rear list holding the newer elements in reverse, whose head is the most recently added^[2]. Both ends are then heads of lists. When the front is empty, the rear is reversed to become the new front.

§ 01

The batched queue

The queue keeps the invariant that the front is empty only if the whole queue is, so the next element is always at the head of the front. Push conses onto the rear; pop takes the head of the front; and both restore the invariant by reversing the rear when the front has become empty.

The queue 1 2 3 4 5 6 as a front and a reversed rear. When the front runs out, the rear is reversed into a new front.

A batched queue, and a banker's queue, with a counter for the work spent reversing.

(* Steps spent reversing, so the demos can measure the cost. *)
let steps = ref 0
let rev l = List.fold_left (fun acc x -> incr steps; x :: acc) [] l
 
(* The batched queue: take from front, add to rear. The front is empty
   only if the whole queue is. *)
module Batched = struct
  type 'a t = { front : 'a list; rear : 'a list }
  let empty = { front = []; rear = [] }
  let check = function
    | { front = []; rear } -> { front = rev rear; rear = [] }
    | q -> q
  let push x q = check { q with rear = x :: q.rear }
  let pop q =
    match q.front with
    | [] -> None
    | x :: front -> Some (x, check { q with front })
end
 
(* The banker's queue: the front is a lazy list, and the rear is
   reversed onto it as soon as it grows longer than the front. *)
module Banker = struct
  type 'a stream = Nil | Cons of 'a * 'a stream Lazy.t
  type 'a t = { front : 'a stream Lazy.t; lenf : int; rear : 'a list; lenr : int }
 
  let rec append s t =
    lazy (match Lazy.force s with
      | Nil -> Lazy.force t
      | Cons (x, s') -> Cons (x, append s' t))
 
  let of_list l = List.fold_right (fun x s -> lazy (Cons (x, s))) l (lazy Nil)
  let empty = { front = lazy Nil; lenf = 0; rear = []; lenr = 0 }
  let check q =
    if q.lenr <= q.lenf then q
    else
      { front = append q.front (lazy (Lazy.force (of_list (rev q.rear))));
        lenf = q.lenf + q.lenr; rear = []; lenr = 0 }
  let push x q = check { q with rear = x :: q.rear; lenr = q.lenr + 1 }
  let pop q =
    match Lazy.force q.front with
    | Nil -> None
    | Cons (x, front) -> Some (x, check { q with front; lenf = q.lenf - 1 })
end

Each element is moved from the rear to the front once, by one reversal step, so $n$ pushes and pops cost $O (n)$ in total: amortized constant time per operation^[4]^[5]. A single reversal can still take $O (n)$ time.

§ 02

Persistence breaks the amortization

The amortized argument assumes that the queue is used linearly, each version once. A functional queue is persistent, and nothing stops a program from popping the same old version repeatedly. If that version has an empty front and a long rear, every pop of it repeats the same expensive reversal.

Each queue used once, then one old version popped 1,000 times.

open Queue
 
let rec drain pop q acc = match pop q with None -> List.rev acc | Some (x, q) -> drain pop q (x :: acc)
 
let n = 100_000

Running it.

order: 1 2 3 4 5 6 7 8 9 10
batched  used once:             100000 reversal steps for 100000 elements
batched  same version x1000:  99999000 reversal steps
banker's used once:             100000 reversal steps for 100000 elements
banker's same version x1000:         0 reversal steps

The batched queue pays the full reversal every time. Okasaki's banker's queue keeps the front as a lazy list and reverses the rear as soon as it becomes longer than the front, appending the reversal to the front as a suspension^[3]^[4]. Every version that shares the suspension shares its result once it has been forced, so repeated pops of an old version do not repeat the work. Reversing when the rear exceeds the front, rather than when the front is empty, guarantees that enough cheap operations happen before the suspension is forced to pay for it. Okasaki's analysis of this with debits, the banker's method, gives amortized $O (1)$ bounds that hold under persistent use^[4].

With further work the reversal can be performed incrementally, a few steps per operation, giving worst-case $O (1)$ queues. Hood and Melville did this without laziness^[1], and Okasaki's real-time queues do it by forcing the lazy front a step at a time^[3].

§ 03

History

Hood and Melville published real-time queues in pure Lisp in 1981^[1], and Burton described the two-list queue with amortized constant-time operations in 1982^[2]. Okasaki showed in 1995 how laziness and memoization make amortized and real-time queues simple to write and correct under persistence^[3], and his 1998 book used queues as the running example for the banker's and physicist's methods of amortized analysis^[4]. OCaml's standard Queue is mutable; the two-list queue is the usual immutable alternative.