5.2.11

题目

Use $f i x$ and the encoding of lists from Exercise 5.2.8 to write a function that sums lists of Church numerals.

第一次写出了这个答案：

s = λ f . λ t . t e s t (i s n i l t) c_{0} (p l u s (h e a d t) (f (t a i l t)))

s u m = f i x s

然而，由于

t r u = λ t . λ f . t

这里不存在常见编程语言的短路特性，由于求值策略是 call-by-value，必须先计算 $f$ 才能应用，也就是最内层 $t = n i l$ 时会对 $(p l u s (h e a d t) (f (t a i l t)))$ 求值，产生错误。

因此，使用 $η$ - 展开，改为：

s = λ f . λ t . t e s t (i s n i l t) (λ x . c_{0}) (λ x . (p l u s (h e a d t) (f (t a i l t)))) c_{0}

s u m = f i x s

这样，所有分支都不会提前求值，直到被选择并应用于 $c_{0}$