Tại sao GHC thực hiện sửa chữa để gây nhầm lẫn?

Question

Nhìn vào mã nguồn GHC tôi có thể thấy rằng định nghĩa cho sửa chữa là:

fix :: (a -> a) -> a 
fix f = let x = f x in x 

Trong một ví dụ sửa chữa được sử dụng như thế này:

fix (\f x -> let x' = x+1 in x:f x') 

này về cơ bản mang lại một chuỗi các con số tăng từ một đến vô cùng. Đối với điều này xảy ra sửa chữa phải được currying chức năng mà nó nhận được quyền trở lại chức năng rất như nó là tham số đầu tiên. Nó không phải là rõ ràng với tôi như thế nào định nghĩa của sửa chữa được liệt kê ở trên có thể được làm điều đó.

Định nghĩa này là làm thế nào tôi đã hiểu thế nào sửa chữa công trình:

fix :: (a -> a) -> a 
fix f = f (fix f) 

Vì vậy, bây giờ tôi có hai câu hỏi:

1. như thế nào x từng đi nghĩa sửa chữa x trong định nghĩa đầu tiên?
2. Có lợi thế nào khi sử dụng định nghĩa đầu tiên trong giây lát không?

Answer 1

Thật dễ dàng để xem cách định nghĩa này hoạt động bằng cách áp dụng lý luận equational.

fix :: (a -> a) -> a 
fix f = let x = f x in x 

Điều gì sẽ x đánh giá đến khi chúng tôi cố gắng để đánh giá fix f? Nó được định nghĩa là f x, vì vậy fix f = f x. Nhưng x ở đây là gì? Đó là f x, giống như trước đây. Vì vậy, bạn nhận được fix f = f x = f (f x). Lý do theo cách này bạn sẽ nhận được một chuỗi các ứng dụng vô hạn của f: fix f = f (f (f (f ...))).

Bây giờ, thay (\f x -> let x' = x+1 in x:f x') cho f bạn nhận được

fix (\f x -> let x' = x+1 in x:f x') 
    = (\f x -> let x' = x+1 in x:f x') (f ...) 
    = (\x -> let x' = x+1 in x:((f ...) x')) 
    = (\x -> x:((f ...) x + 1)) 
    = (\x -> x:((\x -> let x' = x+1 in x:(f ...) x') x + 1)) 
    = (\x -> x:((\x -> x:(f ...) x + 1) x + 1)) 
    = (\x -> x:(x + 1):((f ...) x + 1)) 
    = ... 

Sửa: Về câu hỏi thứ hai của bạn, @ is7s chỉ ra trong các ý kiến ​​rằng định nghĩa đầu tiên là một lợi thế vì nó là hiệu quả hơn.

Để tìm hiểu lý do tại sao, chúng ta hãy nhìn vào cốt lõi cho fix1 (:1) !! 10^8:

a_r1Ko :: Type.Integer  
a_r1Ko = __integer 1 

main_x :: [Type.Integer] 
main_x = 
    : @ Type.Integer a_r1Ko main_x 

main3 :: Type.Integer 
main3 = 
    !!_sub @ Type.Integer main_x 100000000 

Như bạn có thể thấy, sau khi biến đổi fix1 (1:) về cơ bản trở thành main_x = 1 : main_x. Lưu ý cách định nghĩa này đề cập đến chính nó - đây là những gì "buộc nút thắt" có nghĩa là.tự tham chiếu này được biểu diễn như một gián tiếp con trỏ đơn giản trong thời gian chạy:

Bây giờ chúng ta hãy nhìn vào fix2 (1:) !! 100000000:

main6 :: Type.Integer 
main6 = __integer 1 

main5 
    :: [Type.Integer] -> [Type.Integer] 
main5 = : @ Type.Integer main6 

main4 :: [Type.Integer] 
main4 = fix2 @ [Type.Integer] main5 

main3 :: Type.Integer 
main3 = 
    !!_sub @ Type.Integer main4 100000000 

Đây là ứng dụng fix2 thực sự là bảo quản:

Kết quả là phần thứ hai ram cần làm phân bổ cho mỗi phần tử của danh sách (nhưng kể từ khi danh sách được tiêu thụ ngay lập tức, chương trình vẫn chạy một cách hiệu quả trong không gian liên tục):

$ ./Test2 +RTS -s 
    2,400,047,200 bytes allocated in the heap 
     133,012 bytes copied during GC 
      27,040 bytes maximum residency (1 sample(s)) 
      17,688 bytes maximum slop 
       1 MB total memory in use (0 MB lost due to fragmentation) 
[...] 

Hãy so sánh rằng với hành vi của chương trình đầu tiên:

$ ./Test1 +RTS -s   
      47,168 bytes allocated in the heap 
      1,756 bytes copied during GC 
      42,632 bytes maximum residency (1 sample(s)) 
      18,808 bytes maximum slop 
       1 MB total memory in use (0 MB lost due to fragmentation) 
[...] 

Answer 2

Làm thế nào để x có nghĩa là sửa chữa x trong định nghĩa đầu tiên?

fix f = let x = f x in x 

Hãy bindings trong Haskell là đệ quy

Trước hết, nhận ra rằng Haskell phép bindings let đệ quy. Những gì Haskell gọi là "let", một số ngôn ngữ khác gọi là "letrec". Điều này cảm thấy khá bình thường đối với các định nghĩa chức năng. Ví dụ:

ghci> let fac n = if n == 0 then 1 else n * fac (n - 1) in fac 5 
120 

Nhưng nó có vẻ khá lạ đối với định nghĩa giá trị. Tuy nhiên, các giá trị có thể được định nghĩa đệ quy, do tính không nghiêm ngặt của Haskell.

ghci> take 5 (let ones = 1 : ones in ones) 
[1,1,1,1,1] 

Xem A gentle introduction to Haskell mục 3.3 và 3.4 để biết thêm chi tiết về tính lười biếng của Haskell.

thunks trong GHC

Trong GHC, một biểu hiện như-chưa-unevaluated được bọc trong một "thunk": một lời hứa để thực hiện các tính toán. Các khối chỉ được đánh giá khi chúng hoàn toàn là phải là. Giả sử chúng tôi muốn fix someFunction. Theo định nghĩa của fix, đó là

let x = someFunction x in x 

Bây giờ, những gì GHC thấy là một cái gì đó như thế này.

let x = MAKE A THUNK in x 

Vì vậy, vui vẻ tạo một đoạn cho bạn và di chuyển ngay cho đến khi bạn yêu cầu biết thực tế là x.

đánh giá mẫu

Cái vẻ thunk của chỉ xảy ra để đề cập đến bản thân. Hãy lấy ví dụ ones và viết lại để sử dụng fix.

ghci> take 5 (let ones recur = 1 : recur in fix ones) 
[1,1,1,1,1] 

Vậy nội dung đó sẽ như thế nào?
Chúng tôi có thể nội tuyến ones làm chức năng ẩn danh \recur -> 1 : recur để có trình diễn rõ ràng hơn.

take 5 (fix (\recur -> 1 : recur)) 

-- expand definition of fix 
take 5 (let x = (\recur -> 1 : recur) x in x) 

Bây giờ sau đó, những gì làx? Vâng, mặc dù chúng tôi không hoàn toàn chắc chắn x là gì, chúng tôi vẫn có thể đi qua với các ứng dụng chức năng:

take 5 (let x = 1 : x in x) 

Hey nhìn, chúng tôi lại định nghĩa chúng tôi đã có trước đó.

take 5 (let ones = 1 : ones in ones) 

Vì vậy, nếu bạn tin rằng bạn hiểu làm thế nào rằng một công trình, sau đó bạn có một cảm giác tốt về cách fix công trình.

---

Có lợi thế nào để sử dụng định nghĩa đầu tiên trong lần thứ hai?

Có. Vấn đề là phiên bản thứ hai có thể gây ra rò rỉ không gian, ngay cả khi tối ưu hóa. Xem GHC trac ticket #5205, cho một vấn đề tương tự với định nghĩa của forever. Đây là lý do tại sao tôi đề cập đến khối: bởi vì let x = f x in x chỉ phân bổ một đoạn: đoạn x.

Answer 3

Sự khác biệt là chia sẻ và sao chép.

fix1 f = x where x = f x -- more visually apparent way to write the same thing 

fix2 f = f (fix2 f) 

Nếu chúng ta thay thế định nghĩa vào bản thân, cả hai đều giảm so với cùng chuỗi ứng dụng vô hạn f (f (f (f (f ...)))). Nhưng định nghĩa đầu tiên sử dụng cách đặt tên rõ ràng; trong Haskell (như trong hầu hết các ngôn ngữ khác), tính năng chia sẻ được bật bằng khả năng đặt tên cho mọi thứ: một tên ít nhiều được bảo đảm để chỉ một "thực thể" (ở đây, x). Định nghĩa thứ 2 không đảm bảo bất kỳ sự chia sẻ nào - kết quả của cuộc gọi fix2 f được thay thế thành biểu thức, vì vậy nó cũng có thể được thay thế như một giá trị.

Nhưng một trình biên dịch nhất định có thể lý thuyết thông minh về nó và sử dụng chia sẻ trong trường hợp thứ hai.

Sự cố liên quan là "Y bộ kết hợp". Trong giải tích lambda untyped nơi không có đặt tên cấu trúc (và do đó không có tự -reference), Y combinator giả lập tự tài liệu tham khảo bằng cách sắp xếp cho định nghĩa được sao chép, vì vậy đề cập đến các bản sao tự trở thành khả thi. Nhưng trong các triển khai sử dụng mô hình môi trường để cho phép các thực thể được đặt tên trong một ngôn ngữ, tham chiếu trực tiếp theo tên sẽ trở thành có thể.

Để thấy sự khác biệt mạnh mẽ hơn giữa hai định nghĩa, so sánh

fibs1 = fix1 ((0:) . (1:) . g) where g (a:t@(b:_)) = (a+b):g t 
fibs2 = fix2 ((0:) . (1:) . g) where g (a:t@(b:_)) = (a+b):g t 

Xem thêm:

• In Scheme, how do you use lambda to create a recursive function?
• Y combinator discussion in "The Little Schemer"
• Can fold be used to create infinite lists?

(đặc biệt là cố gắng tìm ra hai định nghĩa cuối cùng trong liên kết cuối cùng ở trên).

---

Làm việc từ các định nghĩa, ví dụ bạn fix (\g x -> let x2 = x+1 in x : g x2) chúng tôi nhận

fix1 (\g x -> let x2 = x+1 in x : g x2) 
= fix1 (\g x -> x : g (x+1)) 
= fix1 f where {f = \g x -> x : g (x+1)} 
= fix1 f where {f g x = x : g (x+1)} 
= x  where {x = f x ; f g x = x : g (x+1)} 
= g  where {g = f g ; f g x = x : g (x+1)} -- both g in {g = f g} are the same g 
= g  where {g = \x -> x : g (x+1)}   -- and so, here as well 
= g  where {g x = x : g (x+1)} 

và do đó một định nghĩa đệ quy thích hợp cho g là thực sự tạo ra. (ở trên, chúng tôi viết ....x.... where {x = ...} cho let {x = ...} in ....x...., vì mục đích rõ ràng).

Nhưng nguồn gốc thứ hai tiến hành với một sự phân biệt quan trọng của việc thay thế một giá trị trở lại, không phải là một tên , như

fix2 (\g x -> x : g (x+1)) 
= fix2 f    where {f g x = x : g (x+1)} 
= f (fix2 f)   where {f g x = x : g (x+1)} 
= (\x-> x : g (x+1)) where {g = fix2 f ; f g x = x : g (x+1)} 
= h     where {h x = x : g (x+1) ; g = fix2 f ; f g x = x : g (x+1)} 

nên gọi thực tế sẽ tiến hành như ví dụ

take 3 $ fix2 (\g x -> x : g (x+1)) 10 
= take 3 (h 10)  where {h x = x : g (x+1) ; g = fix2 f ; f g x = x : g (x+1)} 
= take 3 (x:g (x+1)) where {x = 10 ;    g = fix2 f ; f g x = x : g (x+1)} 
= x:take 2 (g x2) where {x2 = x+1 ; x = 10 ; g = fix2 f ; f g x = x : g (x+1)} 
= x:take 2 (g x2) where {x2 = x+1 ; x = 10 ; g = f (fix2 f) ; f g x = x : g (x+1)} 
= x:take 2 (x2 : g2 (x2+1)) where {    g2 = fix2 f ; 
          x2 = x+1 ; x = 10 ;     f g x = x : g (x+1)} 
= ...... 

và chúng ta thấy rằng một mới ràng buộc (đối với g2) được thành lập ở đây, thay vì trước đó (ví g) được tái sử dụng như với định nghĩa fix1.

Answer 4

Tôi có lẽ một lời giải thích đơn giản hóa bit đến từ tối ưu hóa inlining. Nếu chúng ta có

fix :: (a -> a) -> a 
fix f = f (fix f) 

sau đó fix là một hàm đệ quy và điều này có nghĩa là nó không thể được inlined ở những nơi nó được sử dụng (một pragma INLINE sẽ bị bỏ qua, nếu có).

Tuy nhiên

fix' f = let x = f x in x 

là không một hàm đệ quy - nó không bao giờ tự gọi mình. Chỉ có x bên trong là đệ quy.Vì vậy, khi gọi

fix' (\r x -> let x' = x+1 in x:r x') 

trình biên dịch có thể inline nó vào

(\f -> (let y = f y in y)) (\r x -> let x' = x+1 in x:r x') 

và sau đó tiếp tục đơn giản hóa nó, ví dụ

let y = (\r x -> let x' = x+1 in x:r x') y in y 
let y = (\ x -> let x' = x+1 in x:y x') in y 

đó là cũng giống như khi chức năng được xác định sử dụng tiêu chuẩn ký pháp đệ quy không có fix:

y  x = let x' = x+1 in x:y x'