n-ary zip_with

Stream: Is there code for X?

[Floris van Doorn]

Are the following n-ary versions of zip_with useful, or can we already emulate them using a combination of other definitions?

namespace list
variables {α β γ δ ε ζ : Type*}
def zip_with3 (f : α → β → γ → δ) : list α → list β → list γ → list δ
| (x::xs) (y::ys) (z::zs) := f x y z :: zip_with3 xs ys zs
| _       _       _       := []

def zip_with4 (f : α → β → γ → δ → ε) : list α → list β → list γ → list δ → list ε
| (x::xs) (y::ys) (z::zs) (u::us) := f x y z u :: zip_with4 xs ys zs us
| _       _       _       _       := []

def zip_with5 (f : α → β → γ → δ → ε → ζ) : list α → list β → list γ → list δ → list ε → list ζ
| (x::xs) (y::ys) (z::zs) (u::us) (v::vs) := f x y z u v :: zip_with5 xs ys zs us vs
| _       _       _       _       _       := []

end list

[Mario Carneiro]

It's slightly less efficient but zip_with f l1 l2 is equivalent to (roughly) (zip l1 l2).map f and this generalizes to (zip l1 $ zip l2 $ zip l3 l4).map f

[Floris van Doorn]

modulo (un)currying...

[David Wärn]

Haskell goes up to zipWith7 apparently

[Kevin Buzzard]

we could beat that easily

[Floris van Doorn]

I added up to 5 in #7596 (I only needed the 5-ary one)

[David Wärn]

Fwiw you could also do

def zip_with_3 {α β γ δ} (f : α → β → γ → δ) (as : list α) (bs : list β) (cs : list γ) : list δ :=
zip_with id (zip_with f as bs) cs -- `id = ($)`

[David Wärn]

zip_with id, or zipWith ($), is like <*>. It's basically a lift of the binary function ($), and iterating it lets you lift any n-ary function. (zip_with f as can also be written as zip_with id (map f as))

[Floris van Doorn]

Oh, that is indeed a nice definition. In that case, do we still want dedicated n-ary zip_with functions, or shall I remove them from the PR?

[Eric Wieser]

I think it might be worth having them but defining them as David suggests