length

{-
Returns `+1` if the `Optional` value is present and `+0` if the value is absent

Examples:

```
./length Integer ([2] : Optional Integer) = +1

./length Integer ([] : Optional Integer) = +0
```
-}
let length : ∀(a : Type) → Optional a → Natural
    =   λ(a : Type)
    →   λ(xs : Optional a)
    →   Optional/fold a xs Natural (λ(_ : a) → +1) +0

in  length