Purely Functional Queue with Constant Operation Times (Credits to Okasaki)

<pre> :: Queue a = Queue !Int !.[a] !Int !.[.[a]] /* enqLen enqList deqLen deqList */ adjust :: !u:(Queue .a) -> v:(Queue .a), [u <= v] adjust q=:(Queue enqLen enqList deqLen deqList) | enqLen > 3 && enqLen >= deqLen = Queue 0 [] (enqLen + deqLen) (deqList ++ [reverse enqList]) | otherwise = q enq :: .a !u:(Queue .a) -> v:(Queue .a), [u <= v] enq a (Queue enqLen enqList deqLen deqList) = adjust (Queue (enqLen + 1) [a:enqList] deqLen deqList) deq :: !u:(Queue .a) -> (.a, !v:(Queue .a)), [u <= v] deq (Queue enqLen enqList deqLen [[]:deqList]) = deq (Queue enqLen enqList deqLen deqList) deq (Queue enqLen enqList deqLen [[a:as]:deqList]) = (a, adjust (Queue enqLen enqList (deqLen - 1) [as:deqList])) deq (Queue enqLen enqList 0 deqList) = deq (Queue 0 [] enqLen [reverse enqList]) newq :: .(Queue .a) newq = Queue 0 [] 0 [] emptyq :: !.(Queue .a) -> .Bool emptyq (Queue 0 _ 0 _) = True emptyq _ = False </pre>