dhall-1.24.0: dhall-lang/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