dhall-1.26.0: dhall-lang/Prelude/Optional/unzip

{-
Unzip an `Optional` value into two separate `Optional` values
-}
let unzip
    :   ∀(a : Type)
      → ∀(b : Type)
      → Optional { _1 : a, _2 : b }
      → { _1 : Optional a, _2 : Optional b }
    =   λ(a : Type)
      → λ(b : Type)
      → λ(xs : Optional { _1 : a, _2 : b })
      → { _1 =
            Optional/fold
              { _1 : a, _2 : b }
              xs
              (Optional a)
              (λ(x : { _1 : a, _2 : b }) → Some x._1)
              (None a)
        , _2 =
            Optional/fold
              { _1 : a, _2 : b }
              xs
              (Optional b)
              (λ(x : { _1 : a, _2 : b }) → Some x._2)
              (None b)
        }

let example0 =
        assert
      :   unzip Text Bool (Some { _1 = "ABC", _2 = True })
        ≡ { _1 = Some "ABC", _2 = Some True }

let example1 =
        assert
      :   unzip Text Bool (None { _1 : Text, _2 : Bool })
        ≡ { _1 = None Text, _2 = None Bool }

in  unzip