dhall-1.7.0: Prelude/Optional/head

{-
Returns the first non-empty `Optional` value in a `List`

Examples:

```
./head
Integer
(   [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer]
    : List (Optional Integer)
)
= [1] : Optional Integer

./head
Integer
([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer))
= [] : Optional Integer

./head Integer ([] : List (Optional Integer))
= [] : Optional Integer
```
-}
    let head
        : ∀(a : Type) → List (Optional a) → Optional a
        =   λ(a : Type)
          → λ(xs : List (Optional a))
          → List/fold
            (Optional a)
            xs
            (Optional a)
            (   λ(l : Optional a)
              → λ(r : Optional a)
              → Optional/fold a l (Optional a) (λ(x : a) → [ x ] : Optional a) r
            )
            ([] : Optional a)

in  head