哈斯克尔折叠无限列表，使用头部

Question

f :: Int -> [[Int]] -> [[Int]]
f n acc = ([length $ head acc] ++ (take n $ repeat n)) : acc

我试图了解如何

take 2 $ foldr f undefined [0..]

给

[[2],[3,1]]

我能够变身到这里，然后陷入困境

foldr f undefined [0..]
foldr f undefined ([0:[1..])
f 0 $ foldr f undefined [1..]
f 0 $ foldr f undefined (1: [2..])
f 0 $ f 1 $ foldr f undefined [2..]
f 0 $ f 1 $

Answer 1

如果你只展开foldr调用，你永远不会看到任何有趣的东西。一旦对f的调用成为表达式的头部，请改为展开f。该扩展将需要来自其acc的一定数量的信息，这是尾随foldr调用，但它不需要全部信息，因此您将能够取得进展。

...
f 0 $ 
([length $ head (foldr f undefined [1..])] ++ (take 0 $ repeat 0)) : foldr f undefined [1..]
...

在这里，我重复了两次foldr f undefined [1..]，因为acc被使用了两次，但当然你只需要扩展它一次，在两个地方使用相同的结果。

Answer 2

从 f 0 $ f 1 $ foldr f undefined [2..] 开始，再继续一次迭代，然后简单地内联f的定义：

f 0 $ f 1 $ foldr f undefined [2..]
f 0 $ f 1 $ f 2 $ foldr f undefined [3..] -- below let rest = foldr f undefined [3..]
f 0 $ f 1 $ f 2 $ rest
f 0 $ f 1 $ (n acc -> ([length $ head acc] ++ (take n $ repeat n)) : acc) 2 $ rest
f 0 $ f 1 $ (([length $ head rest] ++ (take 2 $ repeat 2)) : rest)
f 0 $ f 1 $ (([length $ head rest] ++ [2,2]) : rest)
f 0 $ f 1 $ ([length $ head rest,2,2] : rest)
f 0 $ (n acc -> ([length $ head acc] ++ (take n $ repeat n)) : acc) 1 $ ([length $ head rest,2,2] : rest)
f 0 $ (([length $ head ([length $ head rest,2,2] : rest)] ++ (take 1 $ repeat 1)) : [length $ head rest,2,2] : rest)
f 0 $ (([length $ [length $ head rest,2,2]] ++ [1]) : [length $ head rest,2,2] : rest) 
-- this is the crux, we don't need to evaluate rest to evaluate the length here
f 0 $ (([3] ++ [1]) : [length $ head rest,2,2] : rest)
f 0 $ ([3,1] : [length $ head rest,2,2] : rest)
((n acc -> ([length $ head acc] ++ (take n $ repeat n)) : acc) 0 $ ([3,1] : [length $ head rest,2,2] : rest)
([length $ head ([3,1] : [length $ head rest,2,2] : rest)] ++ (take 0 $ repeat 0)) : [3,1] : [length $ head rest,2,2] : rest
([length $ [3,1]] ++ []) : [3,1] : [length $ head rest,2,2] : rest
[length $ [3,1]] : [3,1] : [length $ head rest,2,2] : rest
[2] : [3,1] : [length $ head rest,2,2] : rest

现在由于我们只想要前两个元素（take 2），我们得到
[[2],[3,1]]