zip with padding?

Stream: Is there code for X?

[Scott Morrison]

Do we have somewhere the function

partial def List.zipWith' (f : Option α → Option β → γ) : List α → List β → List γ
  | [], [] => []
  | (a :: as), [] => f a none :: zipWith' f as []
  | [], (b :: bs) => f none b :: zipWith' f [] bs
  | (a :: as), (b :: bs) => f a b :: zipWith' f as bs

which is like zipWith but consumes the entirety of both lists, providing none values where necessary?

[Scott Morrison]

I guess

def List.zipWithAll (f : Option α → Option β → γ) : List α → List β → List γ
  | [], [] => []
  | as, [] => as.map fun a => f (some a) none
  | [], bs => bs.map fun b => f none (some b)
  | a :: as, b :: bs => f a b :: zipWithAll f as bs

is better to avoid the partial.

[Damiano Testa]

If you add a Monad List instance, is this close to what you want?

instance : Monad (List) := sorry

variable {α β γ}

def List.zipWithAll3 (f : Option α → Option β → γ) (la : List α) (lb : List β) : List γ :=
(la.zip lb).map fun (a, b) => f a b

EDIT: certainly not, since the zip discards the entries of the longer list.

[Damiano Testa]

Slightly more pertinent to the question at hand, the closest that I could find is docs#List.zipWithLeft' and its neighbours. I could not find a List.zipWithMax' or similar, though...