title: Total real-time persistent queues
body: <p>Okasaki describes persistent real-time queues which can be realized in Haskell using the type</p>
  
  <pre><code>data Queue a = forall x . Queue
    { front :: [a]
    , rear :: [a]
    , schedule :: [x]
    }
  </code></pre>
  
  <p>where incremental rotations maintain the invariant</p>
  
  <pre><code>length schedule = length front - length rear
  </code></pre>
  
  <h3>More details</h3>
  
  <p>If you're familiar with the queues involved, you can skip this section.</p>
  
  <p>The rotation function looks like</p>
  
  <pre><code>rotate :: [a] -&gt; [a] -&gt; [a] -&gt; [a]
  rotate [] (y : _) a = y : a
  rotate (x : xs) (y : ys) a =
    x : rotate xs ys (y : a)
  </code></pre>
  
  <p>and it's called by a smart constructor</p>
  
  <pre><code>exec :: [a] -&gt; [a] -&gt; [x] -&gt; Queue a
  exec f r (_ : s) = Queue f r s
  exec f r [] = Queue f' [] f' where
    f' = rotate f r []
  </code></pre>
  
  <p>after each queue operation. The smart constructor is always called when <code>length s = length f - length r + 1</code>, ensuring that the pattern match in <code>rotate</code> will succeed.</p>
  
  <h3>The problem</h3>
  
  <p>I hate partial functions! I'd love to find a way to express the structural invariant in the types. The usual dependent vector seems a likely choice:</p>
  
  <pre><code>data Nat = Z | S Nat
  
  data Vec n a where
    Nil :: Vec 'Z a
    Cons :: a -&gt; Vec n a -&gt; Vec ('S n) a
  </code></pre>
  
  <p>and then (perhaps)</p>
  
  <pre><code>data Queue a = forall x rl sl . Queue
    { front :: Vec (sl :+ rl) a
    , rear :: Vec rl a
    , schedule :: Vec sl x
    }
  </code></pre>
  
  <p>The trouble is that I haven't been able to figure out how to juggle the types. It seems extremely likely that <em>some</em> amount of <code>unsafeCoerce</code> will be needed to make this efficient. However, I haven't been able to come up with an approach that's even vaguely manageable. Is it possible to do this nicely in Haskell?</p>