/Prelude-v20.0.0/List/unzip.dhall

Copy path to clipboard

Unzip a List into two separate Lists

Examples

  unzip
Text
Bool
[ { _1 = "ABC", _2 = True }
, { _1 = "DEF", _2 = False }
, { _1 = "GHI", _2 = True }
]
≡ { _1 = [ "ABC", "DEF", "GHI" ], _2 = [ True, False, True ] }
  unzip Text Bool ([] : List { _1 : Text, _2 : Bool })
≡ { _1 = [] : List Text, _2 = [] : List Bool }

Source

--| Unzip a `List` into two separate `List`s
let unzip
: ∀(a : Type) →
∀(b : Type) →
List { _1 : a, _2 : b } →
{ _1 : List a, _2 : List b }
= λ(a : Type) →
λ(b : Type) →
λ(xs : List { _1 : a, _2 : b }) →
{ _1 =
List/build
a
( λ(list : Type) →
λ(cons : alistlist) →
List/fold
{ _1 : a, _2 : b }
xs
list
(λ(x : { _1 : a, _2 : b }) → cons x._1)
)
, _2 =
List/build
b
( λ(list : Type) →
λ(cons : blistlist) →
List/fold
{ _1 : a, _2 : b }
xs
list
(λ(x : { _1 : a, _2 : b }) → cons x._2)
)
}

let example0 =
assert
: unzip
Text
Bool
[ { _1 = "ABC", _2 = True }
, { _1 = "DEF", _2 = False }
, { _1 = "GHI", _2 = True }
]
≡ { _1 = [ "ABC", "DEF", "GHI" ], _2 = [ True, False, True ] }

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

in unzip