मैं हास्केल में स्वयं-एप्लिकेशन फ़ंक्शन कैसे लिख सकता हूं?

Question

मैंने कोड का पालन करने की कोशिश की, लेकिन यह टाइप त्रुटियों को उत्पन्न करता है।

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

मुझे नहीं लगता कि एक एकल स्व-अनुप्रयोग फ़ंक्शन है जो हास्केल में सभी शर्तों के लिए काम करेगा। स्व-अनुप्रयोग टाइप किए गए लैम्ब्डा कैलकुस में एक अनोखी चीज है, जो अक्सर टाइपिंग से बच जाएगी। यह तथ्य यह है कि स्वयं आवेदन के साथ हम निश्चित बिंदु Combinator, जो प्रकार प्रणाली जब एक तार्किक प्रणाली के रूप में देखा में विसंगतियों का परिचय व्यक्त कर सकते हैं से संबंधित है (देखें करी-हावर्ड पत्राचार)।

आपने इसे id फ़ंक्शन पर लागू करने के बारे में पूछा। स्वयं आवेदन id id में, दो id रों विभिन्न प्रकार की है। अधिक स्पष्ट रूप से यह (id :: (A -> A) -> (A -> A)) (id :: A -> A) (किसी भी प्रकार के A के लिए) है।

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

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

जो सिर्फ ठीक काम करता है, बल्कि अपने प्रकार द्वारा सीमित है: हम एक स्वयं आवेदन विशेष रूप से id समारोह के लिए बनाया गया हो सकता है।

का उपयोग RankNTypes आप इस तरह स्वयं आवेदन कार्यों के परिवारों बना सकते हैं, लेकिन आप एक सामान्य आत्म आवेदन समारोह ऐसा है कि sa t हो जाएगा t t iff अच्छी तरह से टाइप करने में सक्षम होना करने के लिए नहीं जा रहे हैं अच्छी तरह से आपके द्वारा लिखा गया है (कम से कम सिस्टम Fω ("एफ-ओमेगा") में नहीं, जो जीएचसी का कोर कैलकुस पर आधारित है)।

कारण, यदि आप इस पर काम औपचारिक रूप से (शायद), तो हम sa sa, जो कोई सामान्य रूप है हो सकता है कि है, और Fω सामान्य होने के लिए जाना जाता है (जब तक हम निश्चित रूप से fix जोड़ें)।

Answer 2

उपयोग एक newtype अनंत प्रकार के निर्माण के लिए।

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

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

GHC में, eventually और f स्मृति में एक ही वस्तु हो जाएगा।

Answer 3

इसका कारण यह है untyped लैम्ब्डा पथरी हास्केल से अधिक शक्तिशाली किसी तरह से है। या, इसे अलग-अलग रखने के लिए, untyped lambda कैलकुलेशन में कोई प्रकार की प्रणाली नहीं है। इस प्रकार, इसमें कोई ध्वनि प्रकार प्रणाली नहीं है। जबकि हास्केल में एक है।

यह न केवल स्वयं के आवेदन के साथ दिखाता है, लेकिन किसी भी मामले में जहां अनंत प्रकार शामिल हैं। उदाहरण के लिए यह प्रयास करें,:

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

यह कैसे प्रकार प्रणाली पता चल गया है कि प्रतीत होता है हानिरहित expresion s i i एक ध्वनि प्रकार प्रणाली के साथ अनुमति नहीं होनी चाहिए आश्चर्यजनक है। क्योंकि, अगर यह की अनुमति दी गई, स्वयं आवेदन संभव हो जाएगा।