zipWith.dhall

let NonEmpty = λ(a : Type) → { head : a, tail : List a }
let List2 = λ(a : Type) → < Nil | Cons : NonEmpty a >

let split : ∀(a : Type) → List a → List2 a
    = λ(a : Type)
    → λ(xs : List a)
    → List/fold a xs (List2 a)
        (λ(x : a) → λ(ys : List2 a) →
          merge
          { Cons = λ(cons : NonEmpty a)
                 → < Cons = { head = x, tail = [cons.head] # cons.tail } | Nil>
          , Nil  = < Cons = { head = x, tail = [] : List a } | Nil >
          } ys)
        (List2 a).Nil

let caseList : ∀(a : Type) → List a → ∀(b : Type) → (a → List a → b) → b → b
    = λ(a : Type)
    → λ(xs : List a)
    → λ(b : Type)
    → λ(cons : a → List a → b)
    → λ(nil : b)
    → merge
        { Cons = \(ys : NonEmpty a) -> cons ys.head ys.tail
        , Nil  = nil
        } (split a xs)

let zipWith
    : ∀(a : Type) → ∀(b : Type) → ∀(c : Type)
    → (a → b → c) → List a → List b → List c

    = λ(a : Type) → λ(b : Type) → λ(c : Type)
    → λ(f : a → b → c)
    → λ(xs : List a)
    → λ(ys : List b)
    → List/fold a xs (List b -> List c)
        (\(x : a) -> \(g : List b -> List c) -> \(ys2 : List b) ->
            caseList b ys2 (List c)
              (\(y : b) -> \(ys3 : List b) -> [f x y] # g ys3)
              ([] : List c))
        (\(ys4 : List b) -> [] : List c)
        ys

let zip
    : ∀(a : Type) → ∀(b : Type)
    → List a → List b → List { _1 : a, _2 : b }

    = \(a : Type)
    -> \(b : Type)
    -> zipWith a b { _1 : a, _2 : b }
        (\(x : a) -> \(y : b) -> { _1 = x, _2 = y })

in zip Natural Natural [1, 2, 3] [4, 5, 6, 7]