Tại sao mã Haskell này không chấm dứt?

Question

Tại sao mã Haskell sau không chấm dứt:

foldr (||) True $ repeat False -- never terminates 

khi một cái gì đó như thế này không:

foldr (||) False $ repeat True -- => True 

Đối với tôi, đó là biểu hiện thứ hai để được trông rắc rối hơn không chấm dứt. Có gì sai với quan điểm của tôi về đánh giá lười biếng của Haskell?

Answer 1

Tôi nghĩ rằng sự hiểu biết của bạn về sự lười biếng là chính xác, nhưng không phải cho foldr. Chúng ta hãy nhìn vào nó "specification"

foldr f z [x1, x2, ..., xn] == x1 `f` (x2 `f` ... (xn `f` z)...) 

Sau đó nhìn vào biểu hiện

foldr (||) True $ repeat False -- never terminates 

của bạn Như bạn thấy True (z) mà chúng ta đang "tìm kiếm" để có được || chấm dứt sẽ không được đạt được cho đến khi toàn bộ danh sách được tiêu thụ. Và điều đó sẽ không xảy ra vì danh sách là vô hạn.

Điều này cũng nên giải thích cho ví dụ chấm dứt thực sự.

Answer 2

Mở rộng đầu tiên thành False || (False || (False || ...)), trong khi lần mở rộng thứ hai là True || (True || (True || ...)). Đối số thứ hai cho foldr là một cá trích màu đỏ - nó xuất hiện trong ứng dụng trong cùng của ||, không phải ngoài cùng, do đó, nó có thể không bao giờ thực sự đạt được.

Answer 3

Vấn đề là khá rõ ràng, nếu bạn mở ra các foldr bằng tay:

foldr (||) True $ repeat False == False || (False || (False (False || ... True))) 

Vì vậy, để có được trận chung kết False, mã có để đánh giá danh sách cho đến khi nó (nonexistant) kết thúc. Trong ví dụ thứ hai của bạn, bạn lặp lại True, do đó có thể đánh giá ngắn mạch. Đừng mong đợi ma thuật từ đánh giá lười biếng!

Answer 4

Một thêm một cái nhìn sâu sắc cho bạn là || là không giao hoán trong Haskell, nó thiên vị:

Prelude> undefined || True 
*** Exception: Prelude.undefined 
Prelude> True || undefined 
True 

Vì vậy, không giống như trong toán học, || và flip (||) là chức năng khác nhau. Ví dụ. so sánh

foldr (||) False $ repeat True và foldr (flip (||)) False $ repeat True

Các chấm dứt cựu, nhưng sau này thì không.