Haskell свернуть над бесконечным списком, используя голову

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]]