/Prelude-v22.0.0/List/zip.dhall

Copy path to clipboard

Zip two List into a single List

The resulting List will have the length of the shortest of its arguments.

Examples

  zip Text [ "ABC", "DEF", "GHI" ] Natural [ 1, 2, 3 ]
≡ [ { _1 = "ABC", _2 = 1 }, { _1 = "DEF", _2 = 2 }, { _1 = "GHI", _2 = 3 } ]
zip Text [ "ABC" ] Bool ([] : List Bool) ≡ ([] : List { _1 : Text, _2 : Bool })
zip Text [ "ABC", "DEF", "GHI" ] Natural [ 1 ] ≡ [ { _1 = "ABC", _2 = 1 } ]

Source

{-|
Zip two `List` into a single `List`

The resulting `List` will have the length of the shortest of its arguments.
-}
let List/index =
./index.dhall sha256:e657b55ecae4d899465c3032cb1a64c6aa6dc2aa3034204f3c15ce5c96c03e63
? ./index.dhall

let zip
: ∀(a : Type) → List a → ∀(b : Type) → List b → List { _1 : a, _2 : b }
= λ(a : Type) →
λ(xs : List a) →
λ(b : Type) →
λ(ys : List b) →
let ixs = List/indexed a xs

in List/build
{ _1 : a, _2 : b }
( λ(list : Type) →
λ(cons : { _1 : a, _2 : b } → listlist) →
λ(nil : list) →
List/fold
{ index : Natural, value : a }
ixs
list
( λ(ix : { index : Natural, value : a }) →
λ(rest : list) →
merge
{ None = rest
, Some =
λ(y : b) → cons { _1 = ix.value, _2 = y } rest
}
(List/index ix.index b ys)
)
nil
)

let example0 =
assert
: zip Text [ "ABC", "DEF", "GHI" ] Natural [ 1, 2, 3 ]
≡ [ { _1 = "ABC", _2 = 1 }
, { _1 = "DEF", _2 = 2 }
, { _1 = "GHI", _2 = 3 }
]

let example1 =
assert
: zip Text [ "ABC" ] Bool ([] : List Bool)
≡ ([] : List { _1 : Text, _2 : Bool })

let example2 =
assert
: zip Text [ "ABC", "DEF", "GHI" ] Natural [ 1 ]
≡ [ { _1 = "ABC", _2 = 1 } ]

in zip