dhall-1.42.3: dhall-lang/Prelude/List/unzip.dhall

--| 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 : a → list → list) →
                  List/fold
                    { _1 : a, _2 : b }
                    xs
                    list
                    (λ(x : { _1 : a, _2 : b }) → cons x._1)
              )
        , _2 =
            List/build
              b
              ( λ(list : Type) →
                λ(cons : b → list → list) →
                  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