एक उदाहरण यह है कि कैसे एक डेटा प्रकार हमें किसी भी प्रकार में रहने की अनुमति देता है टर्नर, डीए में दिया जाता है। (2004-07-28), Total Functional Programming, संप्रदाय। 3.1, पेज में 758 नियम 2: प्रकार प्रत्यावर्तन covariant होना चाहिए "
के एक अधिक विस्तृत उदाहरण हास्केल का उपयोग कर करते हैं हम एक साथ शुरू करेंगे।" बुरा "पुनरावर्ती डेटा प्रकार
data Bad a = C (Bad a -> a)
।
और प्रत्यावर्तन के किसी अन्य रूप के बिना इसे से Y combinator निर्माण करते हैं। इसका मतलब है कि इस तरह के एक डेटा प्रकार के होने प्रत्यावर्तन के किसी भी प्रकार का निर्माण, या एक अनंत प्रत्यावर्तन द्वारा किसी भी प्रकार में निवास करने के लिए हमें अनुमति देता है।
,210
untyped लैम्ब्डा पथरी म Y Combinator यह के लिए महत्वपूर्ण है कि हम x x
में खुद को x
लागू के रूप में
Y = λf.(λx.f (x x)) (λx.f (x x))
परिभाषित किया गया है। टाइप की गई भाषाओं में यह सीधे संभव नहीं है, क्योंकि कोई वैध प्रकार x
संभवतः संभवतः नहीं हो सकता है। लेकिन हमारे Bad
डेटा प्रकार इस सापेक्ष जोड़ने/निर्माता को दूर करने की अनुमति देता है:
selfApp :: Bad a -> a
selfApp ([email protected](C x')) = x' x
x :: Bad a
ले जाने पर हम अपने निर्माता खोलने और खुद x
को समारोह के अंदर लागू कर सकते हैं। एक बार जब हम ऐसा करने के तरीके पता है, यह Y Combinator निर्माण करने के लिए आसान है:
yc :: (a -> a) -> a
yc f = let fxx = C (\x -> f (selfApp x)) -- this is the λx.f (x x) part of Y
in selfApp fxx
ध्यान दें कि न selfApp
और न ही yc
पुनरावर्ती हैं, वहाँ अपने आप को एक समारोह का कोई पुनरावर्ती कॉल है। रिकर्सन केवल हमारे रिकर्सिव डेटा प्रकार में दिखाई देता है।
हम जांच सकते हैं कि निर्मित संयोजक वास्तव में ऐसा करता है जो इसे करना चाहिए। हम एक अनंत लूप बना सकते हैं:
loop :: a
loop = yc id
या गणना मान लीजिए कि GCD करते हैं:
gcd' :: Int -> Int -> Int
gcd' = yc gcd0
where
gcd0 :: (Int -> Int -> Int) -> (Int -> Int -> Int)
gcd0 rec a b | c == 0 = b
| otherwise = rec b c
where c = a `mod` b
अच्छा जवाब। मुझे इसके सैद्धांतिक स्पष्टीकरण के साथ इस सुरुचिपूर्ण दृष्टिकोण को पसंद है (अनियमित लैम्ब्डा कैलकुस एम्बेड करना)। क्या इसे विस्तारित करना संभव होगा ताकि यह प्रश्न में भाषा के लिए मनमाने ढंग से पुनरावर्तन प्रदान करे (Agda चलो कहते हैं)? –
@ पेट्रूडलाक तो, मैंने बस अपने officemates के साथ बात की, जो मेरे से बेहतर और दूर बेहतर सिद्धांतवादी हैं। सर्वसम्मति यह है कि यह 'बुरा' प्रकार की अवधि को बढ़ाने के लिए नहीं होगा। ए' (जो आप वास्तव में परवाह करते हैं; रिकर्सन वहां पहुंचने का एक साधन है)। तर्क इस तरह होगा: आप Agda के एक सेट-सैद्धांतिक मॉडल का निर्माण कर सकते हैं; तो आप उस मॉडल को 'Bad' की व्याख्या को एकल-तत्व सेट के रूप में जोड़ सकते हैं; चूंकि परिणामी मॉडल में अभी भी निर्वासित प्रकार हैं, इसलिए किसी अन्य प्रकार की लूपिंग शर्तों में 'खराब' शब्दों को लूपिंग करने का कोई फ़ंक्शन नहीं है। –