/List/unzip.dhall

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 : 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

/Prelude-v21.1.0/List/unzip.dhall

Examples

Source