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.