packages feed

dhall-1.11.0: Prelude/List/unzip

{-
Unzip a `List` into two separate `List`s

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 }
```
-}
    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)
                )
            }

in  unzip