Generic n-ary programs (zipWith, alignWith, lift, etc.) about agda-stdlib HOT 8 CLOSED

open import Category.Applicative using (RawApplicative) hiding (module RawApplicative)

module _ (Test : ∀ {ℓ} → Set ℓ → Set ℓ)
         (raw-applicative : ∀ ℓ → RawApplicative (Test {ℓ})) where

open import Data.Unit
open import Level using (_⊔_; Lift)
open import Data.Nat.Base
open import Data.Product
open import Data.Product.Nary.NonDependent
open import Function
open import Function.Nary.NonDependent

module App {ℓ} = Category.Applicative.RawApplicative (raw-applicative ℓ)

Productκ : ∀ n {l} (as : Sets n (lreplicate n l)) → Set l
Productκ zero    as       = Lift _ ⊤
Productκ (suc n) (a , as) = a × Productκ n as

toProductκ : ∀ n {l} {as : Sets n (lreplicate n l)} → Product⊤ n as → Productκ n as
toProductκ zero    _        = _
toProductκ (suc n) (v , vs) = v , toProductκ n vs

fromProductκ : ∀ n {l} {as : Sets n (lreplicate n l)} → Productκ n as → Product⊤ n as
fromProductκ zero    _        = _
fromProductκ (suc n) (v , vs) = v , fromProductκ n vs

curryκₙ : ∀ n {l} {as : Sets n (lreplicate n l)} {r} {b : Set r} →
          (Productκ n as → b) → as ⇉ b
curryκₙ n f = curry⊤ₙ n (f ∘ toProductκ n)

uncurryκₙ : ∀ n {l} {as : Sets n (lreplicate n l)} {r} {b : Set r} →
            as ⇉ b → (Productκ n as → b)
uncurryκₙ n f = uncurry⊤ₙ n f ∘ fromProductκ n


sequenceA : ∀ n {l} {as : Sets n (lreplicate n l)} →
            Productκ n (Test <$> as) → Test (Productκ n as)
sequenceA zero    p        = App.pure p
sequenceA (suc n) (ta , p) = _,_ App.<$> ta App.⊛ sequenceA n p

lift : ∀ n {l} {R : Set l} {As : Sets n (lreplicate n l)} →
       As ⇉ R → (Test <$> As) ⇉ Test R
lift n f = curryκₙ n (λ ps → uncurryκₙ n f App.<$> sequenceA n ps)

open import Level using (Level)
open import Function
open import Function.Nary.NonDependent
open import Data.Nat
open import Data.Product using (_×_; _,_; proj₁; proj₂) renaming (curry to curry₂; uncurry to uncurry₂)
open import Data.List using (List; []; _∷_; map) renaming (zipWith to zipWith₂)

variable
  l : Level
  R : Set l

zipWith : ∀ n {ls} {as : Sets n ls} →
          Arrows n as R → Arrows n (List <$> as) (List R)
zipWith zero f = []
zipWith (suc zero) f = map f
zipWith (suc (suc n)) f xs₀ xs₁ = zipWith (suc n) id (zipWith₂ f xs₀ xs₁)

zipWith : ∀ n {ls} {as : Sets n ls} →
          Arrows n as R → Arrows n (List <$> as) (List R)
zipWith zero f = []
zipWith (suc zero) f = map f
zipWith (suc (suc n)) f xs₀ xs₁ = zipWith (suc n) (uncurry₂ f) (zipWith₂ _,_ xs₀ xs₁)

zw-aux : ∀ n {ls} {as : Sets n ls} →
         (Product n as → R) →
         (Product n (List <$> as) → List R)
zw-aux 0       f as         = []
zw-aux 1       f (as , _)   = map (f ∘ (_, tt)) as
zw-aux (suc n) f (as , ass) = zipWith _$_ fs as
  where fs = zw-aux n (flip (curry f)) ass