`bind`/`flatMap`/`>>=` over Optional in Dhall

Question

我需要 bind/flatMap/>>= 而不是 Dhall 的 Optional。

我找不到它的实现并想出了我自己的。

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)

然后我按如下方式使用它

bindOptional Outer Inner (λ(x : Outer) → x.inner) outer

Prelude中真的没有定义这样的函数吗？我想我可能错过了。

此外：

1. 有没有更惯用的定义方式？

2. 是否有可能利用类型推断并缩短调用时间？类似的东西

   bindOptional _.inner outer -- the compiler infers `Outer` from `outer` and `Inner` from `_.inner`  
   

我试图不提供类型参数，但似乎不可能（根据我对语言的有限了解）。

Answer 1

在撰写本文时，Prelude 中还没有针对 Optional 的这种操作，尽管没有特别的原因导致它不存在，因此您可以打开拉取请求来添加它。

最接近语言支持的机制是使用 merge 关键字对 Optional 值起作用的事实，所以这会起作用：

merge { Some = λ(_ : Inner) → _.inner, None = None SomeType } outer

...虽然这仍然需要指定 Inner 和 SomeType 类型，所以它不利用类型推断。