उन सभी के लिए धन्यवाद जिन्होंने मेरे प्रश्न का उत्तर दिया। मैंने आपके जवाबों का अध्ययन किया है। यह सुनिश्चित करने के लिए कि मैं समझता हूं कि मैंने जो सीखा है, मैंने अपने प्रश्न का अपना जवाब लिखा है। अगर मेरा जवाब सही नहीं है, तो कृपया मुझे बताएं।
हम k और s के प्रकार के साथ शुरू: (s k) के प्रकार के हस्ताक्षर determing पर
k :: t1 -> t2 -> t1
k = (\a x -> a)
s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5
s = (\f g x -> f x (g x))
चलो पहले काम करते हैं।
याद s की परिभाषा:
s = (\f g x -> f x (g x))
को स्थानापन्न (\f g x -> f x (g x)) करार में kf के लिए परिणाम:
(\g x -> k x (g x))
महत्वपूर्ण जी और एक्स के प्रकार k के अनुरूप होना चाहिए की हस्ताक्षर टाइप करें।
याद रखें कि k इस प्रकार के हस्ताक्षर होते हैं:
k :: t1 -> t2 -> t1
तो, यह समारोह परिभाषा k x (g x) के लिए हमें अपने अनुमान कर सकते हैं:
x के प्रकार k के पहले तर्क के प्रकार है , जो t1 प्रकार है। इसलिए (g x) का परिणाम t2 होना चाहिए
k के दूसरे तर्क के प्रकार, t2 है।
g में x है जो हमारे तर्क के रूप में हमने पहले ही निर्धारित किया है कि t1 टाइप किया गया है। तो (g x) का प्रकार हस्ताक्षर (t1 -> t2) है।
k के परिणाम के प्रकार t1 है, इसलिए (s k) का परिणाम t1 है।
तो, (\g x -> k x (g x)) के प्रकार के हस्ताक्षर यह है:
(t1 -> t2) -> t1 -> t1
इसके बाद, k हमेशा अपने पहले तर्क वापस जाने के लिए परिभाषित किया गया है।तो यह: यह करने के लिए
k x (g x)
अनुबंध:
x
और यह: यह करने के लिए
(\g x -> k x (g x))
अनुबंध:
(\g x -> x)
ठीक है, अब हम बाहर (s k) लगा :
s k :: (t1 -> t2) -> t1 -> t1
s k = (\g x -> x)
अब s (s k) के प्रकार हस्ताक्षर को निर्धारित करते हैं।
हम उसी तरह आगे बढ़ते हैं।
याद s की परिभाषा:
s = (\f g x -> f x (g x))
को स्थानापन्न (\f g x -> f x (g x)) करार में (s k)f के लिए परिणाम:
(\g x -> (s k) x (g x))
महत्वपूर्णg और x के प्रकार (s k) के अनुरूप होना चाहिए की हस्ताक्षर टाइप करें।
याद रखें कि (s k) इस प्रकार के हस्ताक्षर होते हैं:
s k :: (t1 -> t2) -> t1 -> t1
तो, यह समारोह परिभाषा (s k) x (g x) के लिए हमें अपने अनुमान कर सकते हैं:
x के प्रकार (s k) के पहले तर्क के प्रकार है , जो (t1 -> t2) प्रकार है। इसलिए (g x) का परिणाम t1 होना चाहिए
(s k) के दूसरे तर्क के प्रकार, t1 है।
gx है जो इसके तर्क के रूप में है, जिसे हमने पहले ही निर्धारित कर लिया है (t1 -> t2) टाइप किया गया है। तो (g x) का प्रकार हस्ताक्षर ((t1 -> t2) -> t1) है।
(s k) के परिणाम के प्रकार t1 है, इसलिए s (s k) का परिणाम t1 है।
तो, (\g x -> (s k) x (g x)) के प्रकार के हस्ताक्षर यह है:
((t1 -> t2) -> t1) -> (t1 -> t2) -> t1
इससे पहले हम निर्धारित s k इस परिभाषा है:
(\g x -> x)
है यही कारण है कि, यह एक समारोह है कि दो लेता है तर्क और दूसरा लौटाता है।
इसलिए
, इस: यह करने के लिए
(s k) x (g x)
संविदा:
(g x)
और यह: यह करने के लिए
(\g x -> (s k) x (g x))
अनुबंध:
(\g x -> g x)
ठीक है, अब हमने s (s k) का पता लगाया है।
s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1
s (s k) = (\g x -> g x)
अन्त में, इस समारोह के प्रकार के हस्ताक्षर के साथ s (s k) के प्रकार के हस्ताक्षर की तुलना:
p = (\g x -> g x)
p के प्रकार है:
p :: (t1 -> t) -> t1 -> t
p और s (s k) एक ही परिभाषा है (\g x -> g x) तो उनके पास अलग-अलग प्रकार के हस्ताक्षर क्यों हैं?
s (s k) का कारण p से भिन्न प्रकार का हस्ताक्षर है कि p पर कोई बाधा नहीं है। हमने देखा कि s(s k) में k के प्रकार हस्ताक्षर के साथ संगत होने के लिए बाध्य है, और s (s k) में पहले s(s k) के प्रकार हस्ताक्षर के साथ संगत होने के लिए बाध्य है। इसलिए, s (s k) का प्रकार हस्ताक्षर इसके तर्क के कारण बाधित है। भले ही p और s (s k) में समान परिभाषा है g और x पर बाधाएं अलग-अलग हैं।
बाद वाला प्रकार पहले के जैसा ही है, बस कठोर है। क्या 'एक्स' और 'वाई' पर कोई बाधा है? – fuz