Search code examples
haskelltype-inferencefold

Haskell, foldr on infinite list

I got a question while reading LYAH.

Here is my thought of foldr on infinite list:

foldr (:) [] [1..] = 1:2:...:**∞:[]**

I think GHCi does not know it is list before evaluating ∞:[].

But GHCi do know.

So i thought it can recognize foldr (:) [] [infinite list] = [infinite list itself].

Prelude> [1..10] == (take 10 $ foldr (:) [] [1..])
True
Prelude> [1..] == (foldr (:) [] [1..])
Interrupted.

However It wasn't.

I want to know what actually happens when GHCi recognizes it is [1..] before evaluating ∞:[].

Just type inference prior to that evaluation?

Solution

  • I want to know what actually happens when GHCi recognizes it is [1..] before evaluating ∞:[].

    GHCi does not recognizes that it is [1...], this is only the consequence of lazy evaluation.

    foldr is implemented as:

    foldr _ z [] = z
foldr f z (x:xs) = f x (foldr f z xs)

    If you write something like foldr (:) [] [1..], then Haskell does not evalautes this (directly), it only stores that you want to calculate that.

    Now say you for instance want to print (take 3 (foldr (:) [] [1..])) that list, then Haskell is forced to evaluate that, and it will do so by calculating:

    take 3 (foldr (:) [] [1..])
-> take 3 ((:) 1 (foldr (:) [] [2..]))
-> (:) 1 (take 2 (foldr (:) [] [2..]))
-> (:) 1 (take 2 ((:) 2 (foldr (:) [] [3..]))
-> (:) 1 ((:) 2 (take 1 (foldr (:) [] [3..])))
-> (:) 1 ((:) 2 (take 1 ((:) 3 (foldr (:) [] [4..]))))
-> (:) 1 ((:) 2 ((:) 3 (take 0 (foldr (:) [] [4..]))))
-> (:) 1 ((:) 2 ((:) 3 [])

    so it derives [1, 2, 3], and due to Haskell's lazyness, it is not interested in what foldr (:) [] [4..] is. Even if that list would eventually stop, it is simply not evaluated.

    If you calculate something like [1..] = foldr (:) [] [1..], then Haskell will check for list equality, list equality is defined as:

    [] == [] = True
(x:xs) == (y:ys) = x == y && xs == ys
[] == (_:_) = False
(_:_) == [] = False

    So Haskell is forced to unwind the list of the right foldr, but it will keep doing so, until it finds items that are not equal, or one of the list reaches the end. But since each time the elements are equal, and both lists never end, it will never finish, si it will evaluate it like:

       (==) [1..] (foldr (:) [] [1..])
-> (==) ((:) 1 [2..])  ((:) 1 (foldr (:) [] [2..]))

    It sees that both are equal, so it recursively calls:

    -> (==) ((:) 1 [2..])  ((:) 1 (foldr (:) [] [2..]))
-> (==) [2..] foldr (:) [] [2..])
-> (==) ((:) 2 [3..])  ((:) 2 (foldr (:) [] [3..]))
-> (==) [3..] foldr (:) [] [3..])
-> ...

    But as you can see, it will never stop evaluation. Haskell does not know that foldr (:) [] [1..] is equal to [1..], it aims to evaluate it, and since equality forces it to evaluate the entire list, it will get stuck in an infinite loop.

    Yes it would be possible to add a certain pattern in the compiler, such that foldr (:) [] x is replaced with x, and so in the future perhaps a Haskell compiler could return True for these, but this would not solve the problems fundamentally, since if Haskell could derive such things for any type of function (here (:), then it would solve an undecidable problem, hence it is not possible).