I needed to bind
/flatMap
/>>=
over an Optional
in Dhall.
I could not find an implementation for it and came up with my own.
let bindOptional
: ∀(a : Type) → ∀(b : Type) → (a → Optional b) → Optional a → Optional b
= λ(a : Type) →
λ(b : Type) →
λ(f : a → Optional b) →
λ(o : Optional a) →
Prelude.Optional.fold a o (Optional b) f (None b)
which I then use as follows
bindOptional Outer Inner (λ(x : Outer) → x.inner) outer
Is there really no such function defined in the Prelude
? I assume I may have missed it.
Furthermore:
is there a more idiomatic way of defining it?
is it somehow possible to leverage type inference and make the call shorter? Something like
bindOptional _.inner outer -- the compiler infers `Outer` from `outer` and `Inner` from `_.inner`
I attempted to not give the type parameters but it doesn't seem possible (from my limited knowledge of the language).
At the time of this writing there is not such an operation for Optional
in the Prelude, although there is no particular reason why it is absent, so you could open a pull request to add it.
The closest mechanism with language support is to use the fact that the merge
keyword works on Optional
values, so this would work:
merge { Some = λ(_ : Inner) → _.inner, None = None SomeType } outer
… although that still requires specifying the Inner
and SomeType
types, so it does not leverage type inference.