在Dhall中通过bind // flatMap` /`>> =`

问题描述

我需要在Dhall的bind上flatMap / >>= / 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`  
   

我尝试不提供类型参数，但由于我有限的语言知识，这似乎是不可能的。

解决方法

在撰写本文时，尽管没有特殊的原因，但是在序言中Optional中没有这样的操作，因此您可以打开拉取请求来添加它。

支持语言的最接近的机制是使用merge关键字对Optional值有效的事实，因此可以这样做：

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

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