Haskell - Currying? Cần giải thích thêm

Question

Vì vậy, một cái gì đó như

addList :: [int] -> int 
addList = foldl1 (+) 

Tại sao tính năng này hoạt động? Phần Currying. Tại sao không có biến?

Answer 1

Nếu bạn xác định một hàm như f x y = bla, điều này giống với f x = \y -> bla, giống như f = \x -> (\y -> bla). Nói cách khác, f là một hàm lấy một đối số, x và trả về một hàm khác có một đối số là y và sau đó trả về kết quả thực tế. Điều này được gọi là currying.

Tương tự khi bạn làm f x y, nó giống như (f x) y. I E. bạn đang gọi hàm f với đối số x. Điều này trả về một hàm khác, mà bạn áp dụng cho đối số y.

Vì vậy, nói cách khác khi bạn thực hiện addList xs = foldl1 (+) xs, trước tiên bạn gọi số foldl1 (+), sau đó trả về một hàm khác mà bạn áp dụng cho xs. Vì vậy, kể từ khi hàm trả về foldl1 (+) thực sự giống như addList, bạn chỉ có thể rút ngắn nó thành addList = foldl1 (+).

Answer 2

Giải thích từ sepp2k là chính xác, tôi chỉ muốn chỉ ra (ý định chơi chữ) rằng ứng dụng này của currying có tên: Nó được gọi là "kiểu không có điểm". Dưới đây là giải thích tốt, bao gồm các ưu và khuyết điểm: http://www.haskell.org/haskellwiki/Pointfree

Answer 3

Ngoài việc pha cà phê, như đã chỉ ra ở đây, chúng tôi sử dụng cái gọi là eta reduction. Đó là một trong những quy tắc giảm của phép tính lambda là cơ sở của Haskell. Nó nói rằng \x -> f x tương đương với f khi x không xuất hiện trong f.

Cho phép áp dụng cho trường hợp của bạn. Tôi đoán bạn cảm thấy thoải mái với định nghĩa như addList xs = foldl1 (+) xs. Chúng ta có thể viết lại điều này là addList = \xs -> foldl1 (+) xs và bây giờ áp dụng quy tắc giảm eta chúng ta nhận được addList = foldl1 (+).

Quy tắc này dựa trên ý tưởng rằng hai hàm đều bằng nhau nếu chúng cho kết quả như nhau khi được áp dụng cho cùng một đối số. Hai chức năng ở đây là f và g = \x -> f x trong đó f : a -> b và chúng tôi muốn hiển thị rằng đối với tất cả c : a, f c = g c. Để chứng minh nó mất một tùy ý c : a và áp dụng nó cho g: g c = (\x -> f x) c = f c, sự bình đẳng cuối cùng là bởi một quy tắc khác được gọi là giảm beta cho biết rằng ứng dụng chức năng được đánh giá bằng cách thay thế.