An implementation of infinite queues fashioned after the von Neuman ordinals

Queue.agda

open import Data.Nat
open import Data.Maybe
open import Data.Product

-- An implementation of infinite queues fashioned after the von Neuman ordinals

module Queue where

   infixl 5 _⊕_

   data queue (A : Set) : Set where
     ∙ : queue A -- the empty queue
     [_] : A → queue A -- a singleton queue
     _⊕_ : queue A → queue A → queue A -- join two queues, one after the other
     ⟪_⟫ : (ℕ → A × queue A) → queue A -- a queue of infinitely many non-empty queues

   -- push an element to the end of the queue
   push : ∀ {A} → queue A → A → queue A
   push q x = q ⊕ [ x ]

   -- pop the first element off the queue
   pop : ∀ {A} → queue A → Maybe (A × queue A)
   pop ∙ = nothing
   pop [ x ] = just (x , ∙)
   pop (q₁ ⊕ q₂) with pop q₁  | pop q₂
   ...         | nothing      | nothing      = nothing
   ...         | nothing      | just (y , r) = just (y , r)
   ...         | just (x , r) | _            = just (x , r ⊕ q₂)
   pop {A} ⟪ qs ⟫ with (x , q ) ← (qs 0) = just (x , r)
     where
       r : queue A
       r   with pop q
       ... | nothing = ⟪ (λ n → qs (suc n)) ⟫
       ... | just (y , s) = ⟪ (λ {0 → y , s ; (suc n) → qs (suc n)}) ⟫

   -- the queue 0, 1, 2, 3
   example₁ = [ 0 ] ⊕ [ 1 ] ⊕ [ 2 ] ⊕ [ 3 ]

   -- the queue 0, 1, 4, 9, 16, ...
   example₂ = ⟪ (λ n → (n * n , ∙)) ⟫

   -- the queue 0, 2, 4, 6, ..., 3
   example₃ = push ⟪ (λ n → (2 * n , ∙)) ⟫ 3

   -- the queue 0, 2, 4, ..., 1, 3, 5, ...
   example₄ = ⟪ (λ n → (2 * n , ∙)) ⟫ ⊕ ⟪ (λ n → (2 * n + 1 , ∙)) ⟫