Okasaki's real-time queues

Queue.sml

infixr 5 :::

datatype 'a stream = Nil | ::: of 'a * 'a stream lazy

signature QUEUE =
sig
  type 'a queue
  
  val empty : 'a queue
  val snoc : 'a queue * 'a -> 'a queue
  val uncons : 'a queue -> ('a * 'a queue) option
end

structure RealTimeQueue :> QUEUE =
struct
  type 'a triplet = 'a stream * 'a list * 'a stream
  
  (*  Subtypes are structural, not nominal.  *)
  subtype 'a queue of 'a triplet
    = (Nil, nil, Nil)
    | (xs, ys, zs) : 'a queue => (_ ::: $xs, y :: ys, zs)
    | (xs, ys, zs) : 'a queue => (_ ::: $xs, ys, _ ::: $zs)
  
  (*  The inferred type of rotate's argument is:
   *  
   *    subtype 'a rotatable of 'a triplet
   *      = (Nil, _ ::: nil, _)
   *      | (xs, ys, _) : 'a rotatable => (_ ::: $xs, _ :: ys, _)
   *)
  fun rotate (x ::: $xs, y :: ys, zs) = x ::: $rotate (xs, ys, y ::: $zs)
    | rotate (Nil, y :: nil, zs) = y ::: $zs
  
  (*  The inferred type of exec's argument is:
   *  
   *    subtype 'a executable of 'a triplet
   *      = (xs, ys, zs) : 'a queue => (xs, ys, _ ::: $zs)
   *      | (xs, ys, Nil) : 'a rotatable => (xs, ys, Nil)
   *)
  fun exec (xs, ys, _ ::: $zs) = (xs, ys, zs)
    | exec args = let val xs = rotate args in (xs, nil, xs) end
  
  val empty = (Nil, nil, Nil)
  fun snoc ((xs, ys, zs), y) = exec (xs, y :: ys, zs)
  fun uncons (x ::: $xs, ys, zs) = SOME (x, exec (xs, ys, zs))
    | uncons _ = NONE
end