恒定空间短路`foldM`超过`Maybe`

Question

可以说我有以下几点：

f :: b -> a -> b
x :: b
l :: [a]

和

foldl' f x l

在恒定空间中运行。这f是适当严格的。

现在考虑我是否有：

f2 :: b -> a -> Maybe b
f2 x y = if (pred x y) then Just $! (f x y) else Nothing

将要

foldM f2 x l

可靠地在恒定空间中运行？或者我还需要做些什么来确保我有恒定的空间但仍然有短路行为Maybe？

（注意，虽然我问了这个关于 的问题Maybe，但我实际上想用 来做这个Either，但我怀疑方法是相似的）

Answer 1

在库源代码foldM中定义为foldlM，而后者又定义为

foldlM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b
foldlM f z0 xs = foldr c return xs z0
  where c x k z = f z x >>= k

假设，c x k z = f2 z x >>= k，让我们看看调用它时会发生什么。要查看它是否为常量空间，我们将仅通过应用最顶层的函数来减少表达式，而不会减少子表达式。

foldlM f2 z0 (x:xs)
=
foldr c return (x:xs) z0
=
c x (foldr c return xs) z0
=
f2 z0 x >>= foldr c return xs

由于>>=对第一个参数很严格，我们f2 z0 x首先进行评估。如果返回Nothing，我们将忽略其余部分（如您提到的短路）。如果返回Just y，我们有

Just y >>= foldr c return xs
=
foldr c return xs y

我们已准备好进行下一个循环。

这并没有导致我们的术语增长，所以它看起来像是在恒定空间中运行（当然，前提是f2保持大小y不变）。