Làm cách nào để viết chức năng tự ứng dụng trong Haskell?

Question

Tôi đã thử mã sau, nhưng nó tạo ra lỗi loại.

sa f = f f 

• Occurs check: cannot construct the infinite type: t ~ t -> t1 
• In the first argument of ‘f’, namely ‘f’ 
    In the expression: f f 
    In an equation for ‘sa’: sa f = f f 
• Relevant bindings include 
    f :: t -> t1 
     (bound at fp-through-lambda-calculus-michaelson.hs:9:4) 
    sa :: (t -> t1) -> t1 
     (bound at fp-through-lambda-calculus-michaelson.hs:9:1) 

Answer 1

Tôi không nghĩ rằng có một chức năng tự ứng dụng duy nhất sẽ hoạt động cho tất cả các điều khoản trong Haskell. Tự ứng dụng là một điều đặc biệt trong tính toán lambda đã nhập, thường sẽ loại bỏ việc gõ. Điều này liên quan đến thực tế là với việc tự ứng dụng, chúng ta có thể biểu diễn bộ kết hợp điểm cố định, giới thiệu sự mâu thuẫn trong hệ thống kiểu khi được xem như một hệ thống logic (xem thư từ Curry-Howard).

Bạn đã hỏi về việc áp dụng nó cho hàm id. Trong ứng dụng tự id id, hai số id có các loại khác nhau. Rõ ràng hơn là (id :: (A -> A) -> (A -> A)) (id :: A -> A) (đối với bất kỳ loại nào A). Chúng tôi có thể tự tạo một ứng dụng được thiết kế đặc biệt cho chức năng id:

sa :: (forall a. a -> a) -> b -> b 
sa f = f f 

ghci> :t sa id 
sa id :: b -> b 

hoạt động tốt, nhưng bị giới hạn bởi loại hình này.

Sử dụng RankNTypes bạn có thể làm cho các gia đình có chức năng tự ứng dụng như thế này, nhưng bạn sẽ không thể thực hiện chức năng tự ứng dụng chung như vậy sa t sẽ được đánh máy tốt t t. ít nhất là không có trong System Fω ("F-omega"), tính toán cốt lõi của GHC dựa trên).

Lý do, nếu bạn làm việc chính thức (có thể), thì chúng tôi có thể nhận được sa sa, không có hình thức bình thường và Fω được biết là chuẩn hóa (cho đến khi chúng tôi thêm fix tất nhiên).

Answer 2

Sử dụng một Newtype để xây dựng các loại vô hạn.

newtype Eventually a = NotYet (Eventually a -> a) 

sa :: Eventually a -> a 
sa eventually@(NotYet f) = f eventually 

Trong GHC, eventually và f sẽ là cùng một đối tượng trong bộ nhớ.

Answer 3

Điều này là do phép tính lambda chưa được phân loại theo một cách nào đó là nhiều hơn mạnh hơn Haskell. Hoặc, để đặt nó một cách khác, giải tích lambda không định dạng không có hệ thống kiểu. Vì vậy, nó không có hệ thống kiểu âm thanh. Trong khi Haskell có một.

Điều này không chỉ hiển thị với ứng dụng tự, mà trong mọi trường hợp có các loại vô hạn. Hãy thử điều này, ví dụ:

i x = x 
s f g x = f x (g x) 
s i i 

Nó là đáng ngạc nhiên như thế nào hệ thống kiểu phát hiện ra rằng expresion dường như vô hại s i i không nên được cho phép với một hệ thống kiểu âm thanh. Bởi vì, nếu nó được cho phép, tự áp dụng sẽ có thể.