常量空格短路`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的大小不变)。