haskell - GHC 测试套件中的这个简短的内存功能是如何工作的？

Question

Here是以下内存功能的完整可运行代码:

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

两者都计算相同的函数。但是，前者总是(重新)计算 f 0当使用参数 0 调用时.相反，后者将计算 f 0只有第一次使用参数 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 -> = 的左侧，否则我们会丢失内存!

等效地:

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将函数内存为零。然而这是 (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)这将分配另一个 fz对于 1案子。
这看起来不错，但是 fz不会持续很长时间，因为它每次都会重新分配 g' x被称为，否定内存。

为了解决这个问题，我们使用另一个变量，所以 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最多评估一次，将导致分配另一个 fz对于 1案子。这个 fz现在不会消失。

递归地，可以确信现在所有值 f n被内存。