Как эта короткая функция memoization в наборе тестов GHC работает?

Здесь - это полный исполняемый код для следующей функции 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

Я попытался понять это с расширением терминов вручную, но это расширение выглядит так же, как медленная, незамысловатая функция. Как это работает? И как вызывается код с комментариями?

Ответ 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

Оба вычисляют одну и ту же функцию. Тем не менее, первый всегда (re) вычисляет f 0 при вызове с аргументом 0. Вместо этого последний будет вычислять f 0 только в первый раз, когда он вызывается с аргументом 0 - когда это произойдет, fz оценивается и результат сохраняется там навсегда, так что его можно снова использовать повторно в следующий раз fz.

Это не слишком отличается от

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

где последний вызовет f 0 только один раз, так как второй раз fz будет уже оценен.

Таким образом, мы могли бы получить свежую memoization 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

Теперь это только memoizes 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. Таким образом, мы получили memoization вместо 1!

Следовательно, мы можем рекурсировать

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, сохраняя его memoizing.

Если вызвано с 1, это вызовет g (f . succ), который выделит другой fz для случая 1. Это выглядит хорошо, но 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 оценивается не более одного раза и приведет к выделению другого fz для случая 1. Этот fz теперь не исчезнет.

Рекурсивно можно убедиться, что теперь все значения f n запоминаются.