dhall-1.3.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  }
    ]   : List { _1 : Text, _2 : Bool }
)
=   { _1 = ["ABC", "DEF", "GHI"] : List Text
    , _2 = [True, False, True] : List Bool
    }

./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