GHC测试套件中的这个简短的记忆功能是如何工作的？

Question

Here是以下memoization函数的完整可运行代码：

memo f = g
  where
    fz = f Z
    fs = memo (f . S) 
    g  Z    = fz
    g (S n) = fs n
    -- It is a BAD BUG to inline 'fs' inside g
    -- and that happened in 6.4.1, resulting in exponential behaviour

-- memo f = g (f Z) (memo (f . S))
--        = g (f Z) (g (f (S Z)) (memo (f . S . S)))
--        = g (f Z) (g (f (S Z)) (g (f (S (S Z))) (memo (f . S . S . S))))

fib' :: Nat -> Integer
fib'             =  memo fib
  where
  fib Z          =  0
  fib (S Z)      =  1
  fib (S (S n)) = fib' (S n) + fib' n

我试图通过手动扩展术语来解决这个问题，但扩展看起来就像是一个缓慢的、无记忆的函数。它怎麽工作?那么注释掉的代码是如何派生的呢？

Answer 1

这很难解释。我将从一个更简单的示例开始。

我们必须牢记两者之间的区别

\x -> let fz = f 0 in if x==0 then fz else f x
let fz = f 0 in \x -> if x==0 then fz else f x

两者都计算相同的函数。但是，当使用参数0调用时，前者总是(重新)计算f 0。相反，后者将只在第一次使用参数0调用它时计算f 0 --当发生这种情况时，将计算fz，并将结果永久存储在那里，以便下次需要fz时可以再次重用它。

这并没有太大的区别

f 0 + f 0
let fz = f 0 in fz + fz

其中后者将只调用f 0一次，因为第二次fz已经被计算过了。

因此，我们可以实现f的轻量级内存，只存储f 0，如下所示：

g = let fz = f 0 in \x -> if x==0 then fz else f x

等同的：

g = \x -> if x==0 then fz else f x
   where
   fz = f 0       

注意，这里我们不能把\x ->放在=的左边，否则我们会丢失memoization！

等同的：

g = g' 
   where
   fz = f 0       
   g' = \x -> if x==0 then fz else f x

现在我们可以把\x ->放在左边，没有任何问题。

等同的：

g = g' 
   where
   fz = f 0       
   g' x = if x==0 then fz else f x

等同的：

g = g' 
   where
   fz = f 0       
   g' 0 = fz
   g' x = f x

现在，这只记录了f 0，而不是每个f n。实际上，计算两次g 4将导致计算两次f 4。

为了避免这种情况，我们可以开始让g在任何函数f上工作，而不是固定的函数：

g f = g'    -- f is now a parameter
   where
   fz = f 0       
   g' 0 = fz
   g' x = f x

现在，我们利用这一点：

-- for any f, x
g f x = f x
-- hence, in particular
g (f . succ) (pred x) = (f . succ) (pred x) = f (succ (pred x)) = f x

因此，g (f . succ) (pred x)是一种编写f x的复杂方式。与往常一样，g将该函数记在0处。然而，这是(f . succ) 0 = f 1。通过这种方式，我们在1获得了memoization！

因此，我们可以递归

g f = g'    -- f is now a parameter
   where
   fz = f 0       
   g' 0 = fz
   g' x = g (f . succ) (pred x)

如果使用0调用，则使用fz存储f 0，并对其进行记忆。

如果使用1调用，这将调用g (f . succ)，它将为1案例分配另一个fz。这看起来不错，但fz不会持续很长时间，因为每次调用g' x时都会重新分配它，从而否定了memoization。

为了解决这个问题，我们使用了另一个变量，这样g (f . succ)最多只会计算一次。

g f = g'    -- f is now a parameter
   where
   fz = f 0       
   fs = g (f . succ)
   g' 0 = fz
   g' x = fs (pred x)

在这里，fs最多评估一次，并将导致为1情况分配另一个fz。这个fz现在不会消失了。

通过递归方式，我们可以确信现在所有的值f n都被记忆了。