让我们考虑以下模块签名：

module Test {a b} (A : Set a) (B : Set b) where

它允许定义以下功能类型：

τ₁ : Set _
τ₁ = A → B → Maybe B

τ₂ : Set _
τ₂ = List A → B → Maybe B

我想写一个优雅的函数，将f类型的元素τ₁转换为g类型的元素τ₂。我希望g是f的扩展，因为它将对f作为参数的列表中的每个元素应用g。我的第一次尝试是：

factor₁ : τ₁ → τ₂
factor₁ _ [] b = return b
factor₁ f (x ∷ l) b = f x b >>= factor₁ f l

从某种意义上讲它有点优雅，因为它使用了monad来链接函数调用。但是通过编写这段代码，我觉得这个函数必须已经作为元函数存在于标准库中的某个地方，但是我没有找到这样的函数。我什至在List文件中寻找函数，这导致使用foldr进行第二次尝试（也可以使用foldl完成）：

factor₂ : τ₁ → τ₂
factor₂ f l b = foldr (λ x → maybe (f x) nothing) (just b) l

但是，我不喜欢此功能，因为它不那么优雅，并且不使用monad机制。但是它有其优点：它包含一个来自标准库的单个函数调用，这是我认为可能的。过了一会儿，我意识到，如果我稍微调整一下原始类型，如下所示：

τ₁' : Set _
τ₁' = A → Maybe B → Maybe B

τ₂' : Set _
τ₂' = List A → Maybe B → Maybe B

该函数将非常简单而优雅：

factor₃ : τ₁' → τ₂'
factor₃ f = flip (foldr f)

但是，这些不是我想要使用的类型，并且与例如使用单声道的普通呼叫链不匹配。

我的问题如下：

• 标准库中是否存在这样的功能？
• 如果否，是否会有更优雅的书写方式？

此外，这是我模块的标题，以便使此示例自包含：

open import Data.List
open import Data.Maybe
open import Data.Maybe.Categorical
open import Category.Monad
open import Function

module Test {a b} (A : Set a) (B : Set b) where

open RawMonad {f = b} monad 

编辑：我发现了一种写符合我的要求的因子函数的新方法：

factor : τ₁ → τ₂
factor f l b = foldl (λ x → (x >>=_) ∘ f) (return b) l

但是，我仍然不知道标准库中是否存在这种功能，或者是否可以将其编写为更高杠杆功能的实例。