Agda-stdlib: Generic n-ary programs (zipWith, alignWith, lift, etc.)

[mechvel]

I wonder of wherher the library needs some generalized zipWith-n functions.
For example, the below function is actually zipWith3,
but one list is by List and others are by List.All:

   zip3with? : (triples : List (C × ℕ × C))  →  All.All ^eq triples  →
                    All.All (\e → e > 0) $ map tuple32 triples  →  List Item 
    zip3with? [] _ _  =  []
    zip3with? ((p , e , d) ∷ triples) (d=p^e ∷a eqs) (e>0 ∷a restExps>0) =
                                                      item ∷ (zip3with? triples eqs restExps>0)
                                                     where
                                                     item = record{ ... } 

[MatthewDaggitt]

So off the top of my head I'm struggling to come up with a generalised zipWith-n function which is both sufficiently general and easy to reason about. Do you have such an implementation?

I don't think zip3with is common or useful enough to warrant being included in the standard library.

[MatthewDaggitt]

Closing as I'm afraid I can't come up with a suitable zipWith-n function.

[gallais]

I think this ought to be doable using the code in #608

Edit: yep. uncurried version (_<$>_ is map over Sets using a level polymorphic endofunctor on Set l):

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

[jespercockx]

How about

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₁)

or alternatively

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₁)

[gallais]

I like the second one better. I am puzzled because I tried my best and I really
could not see how to implement it.

[MatthewDaggitt]

Going to remove the v1.1 milestone for this as I don't think it's urgent.

[gallais]

Generic n-ary lift for applicatives following a discussion with @Zambonifofex

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)