Zipping with foldr in linear time.

ZipFolds.agda

open import Data.Nat
open import Data.List hiding (foldr)
open import Function
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Data.Product

foldr :
    {A : Set}
    (B : List A → Set)
  → (∀ {xs} x → B xs → B (x ∷ xs))
  → B []    
  → (xs : List A)
  → B xs
foldr B f z []       = z
foldr B f z (x ∷ xs) = f x (foldr B f z xs)

Zip1 : Set → Set → Set → ℕ → Set
Zip1 A B C zero    = C → List (A × B)
Zip1 A B C (suc n) = (A → Zip1 A B C n → List (A × B)) → List (A × B)

Zip2 : Set → Set → Set → ℕ → Set
Zip2 A B C zero    = A → C → List (A × B)
Zip2 A B C (suc n) = A → (Zip2 A B C n → List (A × B)) → List (A × B)

unifyZip : ∀ A B n m → ∃₂ λ C₁ C₂ → Zip1 A B C₁ n ≡ (Zip2 A B C₂ m → List (A × B))
unifyZip A B zero    m       = Zip2 A B ⊥ m , ⊥ , refl
unifyZip A B (suc n) zero    = ⊥ , Zip1 A B ⊥ n , refl
unifyZip A B (suc n) (suc m) with unifyZip A B n m
... | C₁ , C₂ , p = C₁ , C₂ , cong (λ t → (A → t → List (A × B)) → List (A × B)) p

zip1 : ∀ A B C (as : List A) → Zip1 A B C (length as)
zip1 A B C = foldr (Zip1 A B C ∘ length) (λ x r k → k x r) (λ _ → [])

zip2 : ∀ A B C (bs : List B) → Zip2 A B C (length bs)
zip2 A B C = foldr (Zip2 A B C ∘ length) (λ y k x r → (x , y) ∷ r k) (λ _ _ → [])
  
zipp : ∀ {A B : Set} → List A → List B → List (A × B)
zipp {A}{B} xs ys with unifyZip A B (length xs) (length ys)
... | C₁ , C₂ , p with zip1 A B C₁ xs | zip2 A B C₂ ys
... | zxs | zys rewrite p = zxs zys