Why are append and uncons for catenable lists merely amortized O(1)?

Question

I took Okasaki's implementation of catenable lists, and refactored it a little bit to avoid Boolean blindness issues. Other than that, the data structure itself remains unchanged:

functor CatList (Q : QUEUE) :> CAT_LIST =
struct
  (* private stuff, not exposed by CAT_LIST *)

  structure L = Lazy
  structure O = Option  (* from basis library *)

  datatype 'a cons = ::: of 'a * 'a cons L.lazy Q.queue

  infixr 5 :::

  (* Q.snoc : 'a Q.queue * 'a -> 'a Q.queue *)
  fun link (x ::: xs, ys) = x ::: Q.snoc (xs, ys)

  (* L.delay : ('a -> 'b) -> ('a -> 'b L.lazy)
   * L.force : 'a L.lazy -> 'a
   * Q.uncons : 'a Q.queue -> ('a * 'a Q.queue lazy) option *)
  fun linkAll (xs, ys) =
    let
      val xs = L.force xs
      val ys = L.force ys
    in
      case Q.uncons ys of
          NONE => xs
        | SOME ys => link (xs, L.delay linkAll ys)
    end

  (* public stuff, exposed by CAT_LIST *)

  type 'a list = 'a cons option

  val empty = NONE

  (* L.pure : 'a -> 'a L.lazy *)
  fun append (xs, NONE) = xs
    | append (NONE, xs) = xs
    | append (SOME xs, SOME ys) = SOME (link (xs, L.pure ys))

  (* Q.empty : 'a Q.queue *)
  fun cons (x, xs) = append (SOME (x ::: Q.empty), xs)
  fun snoc (xs, x) = append (xs, SOME (x ::: Q.empty))

  (* O.map : ('a -> 'b) -> ('a option -> 'b option) *)
  fun uncons NONE = NONE
    | uncons (SOME (x ::: xs)) = SOME (x, L.delay (O.map linkAll) (Q.uncons xs))
end

In his book, Okasaki claims that, given an implementation of queues with O(1) operations (either worst-case or amortized), append and uncons are amortized O(1).

Why can't his claim be strengthened? Given an implementation of real-time queues (all operations are worst-case O(1)), append and uncons look worst-case O(1) to me. All recursive calls in linkAll are guarded by L.delay, and none of the public operations ever forces more than one suspension. Is my reasoning (or my code) wrong?

Answer 1

Regarding your question on catenable lists. You need to also take into account that forcing a suspension may result in a cascade of forces. Note that linkAll forces its input list, which could be a yet unevaluated suspension 's'. Forcing 's' may in turn force another suspension and so on. This would indeed happen if you do a sequence of uncons operations on the list. Eventually, at most after 'n' uncons operations, the data structure may degenerate to the naive Cons list (Cons(x, Cons(y, ...))), where 'n' is the size of the list. Any further uncons operations will have constant time. Therefore the data structure does have an amortized constant time bound, but it is not worst case.