मेरे पास हास्केल को "अपमानजनक" के रूप में प्रतिबंधित करने के बारे में बहुत अच्छी अंतर्ज्ञान है: अर्थात् forall-> के अलावा किसी प्रकार के निर्माता के तर्क में प्रकट होता है। लेकिन भविष्यवाणी क्या है? क्या यह महत्वपूर्ण बनाता है? यह "predicate" शब्द से कैसे संबंधित है?पूर्वानुमान क्या है?
मुझे "एटिमोलॉजी" मुद्दे के बारे में एक बिंदु जोड़ने दो, क्योंकि @DanielWagner के दूसरे उत्तर में तकनीकी आधार शामिल है।
a जैसे कुछ पर अनुमान a -> Bool है। अब एक अनुमानित तर्क वह है जो भविष्यवाणी के बारे में कुछ समझ में आता है - इसलिए यदि हमारे पास कुछ अनुमान P है और हम किसी दिए गए a, P(a) के लिए, "भविष्यवाणी तर्क" (जैसे प्रथम क्रम तर्क) के बारे में बात कर सकते हैं) हम ∀a. P(a) भी कह सकते हैं। इसलिए हम चर पर मात्रा निर्धारित कर सकते हैं और ऐसी चीजों पर भविष्यवाणियों के व्यवहार पर चर्चा कर सकते हैं।
अब, हम कहते हैं कि एक बयान भविष्यवाणी है यदि सभी चीजों को भविष्यवाणी करने के लिए पूर्व पेश किया गया है। तो बयान "चीजों पर आधारित" हैं जो पहले से मौजूद हैं। बदले में, एक कथन अप्रासंगिक है अगर कुछ अर्थों में इसे अपने "बूटस्ट्रैप्स" से संदर्भित किया जा सकता है।
तो उदा। ऊपर id उदाहरण के लिए, हम पाते हैं कि हम है कि यह प्रकार id की की कुछ और करने के लिए id की प्रकार के बारे में कुछ लेता है id इस तरह करने के लिए एक प्रकार दे सकते हैं। तो अब हम एक फ़ंक्शन को एक प्रकार दे सकते हैं जहां एक क्वांटिफाइड वेरिएबल (forall a. द्वारा पेश किया गया) पूरे फ़ंक्शन के समान प्रकार के रूप में "विस्तार" कर सकता है!
इसलिए अप्रत्याशितता एक निश्चित "आत्म संदर्भ" की संभावना पेश करती है। लेकिन रुको, आप कह सकते हैं, क्या ऐसी चीज विरोधाभास का कारण नहीं बनती? जवाब है: "ठीक है, कभी-कभी।" विशेष रूप से, "सिस्टम एफ" जो पॉलिमॉर्फिक लैम्ब्डा कैलकुलास है और जीएचसी की "कोर" भाषा का आवश्यक "कोर" अपर्याप्तता का एक रूप प्रदान करता है, फिर भी दो स्तर होते हैं - मूल्य स्तर, और प्रकार का स्तर, जिसे अनुमति है खुद पर मात्राबद्ध करें। इस दो-स्तरीय स्तरीकरण में, हम अपर्याप्तता और विरोधाभास/विरोधाभास नहीं कर सकते हैं।
हालांकि टिप्पणी बहुत नाजुक और अधिक सुविधाओं के अलावा द्वारा पेंच के लिए, ओलेग द्वारा लेख के इस संग्रह के रूप में आसान इंगित करता है कि यह साफ चाल है: http://okmij.org/ftp/Haskell/impredicativity-bites.html
इन प्रकार के सिस्टम का केंद्रीय प्रश्न यह है: "क्या आप एक प्रकार के चर के लिए एक पॉलिमॉर्फिक प्रकार को प्रतिस्थापित कर सकते हैं?"। पूर्वानुमानित प्रकार के सिस्टम गैर-बकवास स्कूलीमार्म उत्तर देने वाले हैं, "बिलकुल नहीं", जबकि अपमानजनक प्रकार के सिस्टम आपके निस्संदेह दोस्त हैं जो सोचते हैं कि एक मजेदार विचार की तरह लगता है और संभवतः क्या गलत हो सकता है?
अब, हास्केल चर्चा को थोड़ा सा हल करता है क्योंकि इसका मानना है कि बहुरूपता उपयोगी लेकिन अदृश्य होनी चाहिए। इसलिए इस पोस्ट के शेष भाग के लिए, मैं हास्केल की बोली में लिखूंगा जहां forall के उपयोग की अनुमति नहीं है बल्कि आवश्यक है। इस तरह हम a प्रकार के बीच अंतर कर सकते हैं, जो एक मोनोमोर्फिक प्रकार है जो टाइपिंग पर्यावरण से अपना मूल्य खींचता है जिसे हम बाद में परिभाषित कर सकते हैं, और प्रकार forall a. a, जो कि रहने के लिए कठिन पॉलीमोर्फिक प्रकारों में से एक है। हम forall को किसी प्रकार में कहीं भी कहीं भी जाने की अनुमति देंगे - जैसा कि हम देखेंगे, जीएचसी तकनीकी प्रकार की आवश्यकता के बजाय "असफल-तेज" तंत्र के रूप में अपने प्रकार के सिंटैक्स को प्रतिबंधित करता है।
मान लीजिए कि हमने कंपाइलर id :: forall a. a -> a बताया है। क्या हम बाद में id का उपयोग करने के लिए कह सकते हैं जैसे कि (forall b. b) -> (forall b. b) टाइप किया गया हो? इसके साथ असंभव प्रकार के सिस्टम ठीक हैं, क्योंकि हम id के प्रकारमें क्वांटिफ़ायर को तत्काल कर सकते हैं, और परिणामस्वरूप के लिए forall b. b को प्रतिस्थापित कर सकते हैं। प्रेडीकेटिव प्रकार सिस्टम में थोड़ा और अधिक है कि से सावधान कर रहे हैं: केवल monomorphic प्रकार में अनुमति दी जाती है
वहाँ एक ऐसी ही कहानी के बारे में [] :: forall a. [a] और (:) :: forall a. a -> [a] -> [a] है। (तो अगर हम एक विशेष b था, हम id :: b -> b लिख सकते हैं।)। जबकि आपका निस्संदेह दोस्त [] :: [forall b. b] और (:) :: (forall b. b) -> [forall b. b] -> [forall b. b] के साथ ठीक हो सकता है, भविष्यवाणी करने वाला स्कूलीमार्ग इतना नहीं है। वास्तव में, जैसा कि आप सूचियों के केवल दो रचनाकारों से देख सकते हैं, वहां पॉलिमॉर्फिक मान वाले सूचियों को उत्पन्न करने के लिए पॉलिमॉर्फिक मान वाले सूचियों का उत्पादन करने के लिए कोई तरीका नहीं है। इसलिए टाइप [forall b. b]हैस्केल की हमारी बोली में की अनुमति है, यह वास्तव में समझदार नहीं है - उस प्रकार की कोई (समाप्ति) शर्तें नहीं हैं। यह शिकायत करने के जीएचसी के फैसले को प्रेरित करता है अगर आप इस प्रकार के बारे में भी सोचते हैं - यह आपको "परेशान न करें" कहने का संकलक का तरीका है। *
ठीक है, स्कूलमार्म इतना सख्त बनाता है? सामान्य रूप से, उत्तर टाइप-चेकिंग और टाइप-इनफरेंस को करने योग्य रखने के बारे में है। अपमानजनक प्रकारों के लिए अनुमान टाइप करें सही है। टाइपिंग seems like it might be possible टाइप करें, लेकिन यह खूनी जटिल है और कोई भी इसे बनाए रखना चाहता है।
दूसरी ओर, कुछ आपत्ति हो सकता है कि GHC कुछ प्रकार है कि आवश्यकता के लिए impredicativity दिखाई साथ पूरी तरह से खुश है:
> :set -Rank2Types
> :t id :: (forall b. b) -> (forall b. b)
{- no complaint, but very chatty -}
ऐसा लगता है कि impredicativity के कुछ थोड़ा-प्रतिबंधित संस्करणों बहुत बुरा नहीं हैं: विशेष रूप से , प्रकार-जांच उच्च-रैंक प्रकार (जो कि प्रकार चर को पॉलीमोर्फिक प्रकारों द्वारा प्रतिस्थापित करने की अनुमति देते हैं, जब वे केवल (->) पर तर्क हैं) अपेक्षाकृत सरल है। आप रैंक -2 के ऊपर टाइप अनुमान, और रैंक -1 के ऊपर मूल प्रकार खो देते हैं, लेकिन कभी-कभी उच्च रैंक प्रकार डॉक्टर द्वारा आदेश दिए जाते हैं।
शब्द के व्युत्पत्ति के बारे में डुनो, यद्यपि!
* आप आश्चर्य हो सकता है आप कुछ इस तरह कर सकते हैं या नहीं:
data FooTy a where
FooTm :: FooTy (forall a. a)
तो फिर तुम एक शब्द (FooTm) जिसका प्रकार (->) के अलावा कुछ के लिए कुछ तर्क के रूप में बहुरूपी था मिलेगा (अर्थात्, FooTy), आपको ऐसा करने के लिए स्कूलीमार्ग को पार करने की आवश्यकता नहीं है, और इसलिए विश्वास "गैर-(->) पॉलिमॉर्फिक प्रकारों के लिए सामान लागू करना उपयोगी नहीं है क्योंकि आप उन्हें नहीं बना सकते" को अमान्य कर दिया जाएगा। जीएचसी आपको FooTy लिखने नहीं देता है, और मैं स्वीकार करूंगा कि मुझे यकीन नहीं है कि प्रतिबंध के लिए कोई सिद्धांत है या नहीं।
मैं चाहूँगा पर एक टिप्पणी करने के लिए व्युत्पत्ति विज्ञान मुद्दा, चूंकि @ एससीएलवी का जवाब बिल्कुल सही नहीं है (व्युत्पन्न रूप से, अवधारणात्मक रूप से नहीं)।
रसेल के दिनों में समय पर वापस जाएं, जब सबकुछ सिद्धांत स्थापित होता है- तर्क सहित।विशेष आयात के तार्किक विचारों में से एक "समझ का सिद्धांत" है; अर्थात, कुछ तार्किक भविष्यवाणी φ:A→2 दी गई है, हम उस सिद्धांत को संतुष्ट करने वाले सभी तत्वों के सेट को निर्धारित करने के लिए कुछ सिद्धांत चाहते हैं, जिसे "{x | φ(x) }" या उसमें कुछ भिन्नता के रूप में लिखा गया है। ध्यान में रखना महत्वपूर्ण बात यह है कि "सेट" और "भविष्यवाणी" को मौलिक रूप से अलग-अलग चीजों के रूप में देखा जाता है: भविष्यवाणी वस्तुओं से सच्चे मूल्यों में मैपिंग होती है, और सेट वस्तुएं होती हैं। इस प्रकार, उदाहरण के लिए, हम सेट पर मात्रा निर्धारित करने की अनुमति दे सकते हैं लेकिन भविष्यवाणियों पर मात्रा निर्धारित नहीं कर सकते हैं।
अब, रसेल अपने नामित विरोधाभास से चिंतित थे, और इससे छुटकारा पाने के लिए कुछ रास्ता मांगा। कई फिक्स हैं, लेकिन यहां रुचि का एक सिद्धांत समझ के सिद्धांत को सीमित करना है। लेकिन सबसे पहले, सिद्धांत की औपचारिक परिभाषा: ∃S.∀x.S x ↔︎ φ(x); अर्थात, हमारे विशेष φ के लिए कुछ ऑब्जेक्ट (यानी सेट) S मौजूद है जैसे कि प्रत्येक ऑब्जेक्ट (एक सेट, लेकिन एक तत्व के रूप में सोचा जाता है) x, हमारे पास S x है (आप इसे "x∈S" के रूप में सोच सकते हैं ", हालांकि उस समय के तर्ककर्ताओं ने" ∈ "केवल juxtaposition की तुलना में एक अलग अर्थ दिया) φ(x) के मामले में सच है। यदि हम सिद्धांत को बिल्कुल लिखित रूप में लेते हैं तो हम एक अपमानजनक सिद्धांत के साथ समाप्त होते हैं। हालांकि, हम उन प्रतिबंधों को रख सकते हैं जिन पर φ हमें समझने की अनुमति है। (उदाहरण के लिए, यदि हम कहते हैं कि φ में कोई दूसरा ऑर्डर क्वांटिफायर नहीं होना चाहिए।) इस प्रकार, किसी भी प्रतिबंध R के लिए, यदि सेट R -predicate द्वारा निर्धारित किया गया है (यानी, समझ के माध्यम से उत्पन्न), तो हम कहते हैं कि S "R -प्रैडिएटिव" है। यदि हमारी भाषा में प्रत्येक सेट R है - तो हम कहते हैं कि हमारी भाषा "R -Predicative" है। और फिर, जैसा कि अक्सर हाइफेनेटेड उपसर्ग चीजों के मामले में होता है, उपसर्ग को छोड़ दिया जाता है और "अनुमानित" भाषाओं से अंतर्निहित छोड़ दिया जाता है। और, स्वाभाविक रूप से, जो भाषाएं भविष्यवाणी नहीं हैं वे "अपमानजनक" हैं।
यह पुराना स्कूल व्युत्पत्ति है। उन दिनों से शर्तें बंद हो गई हैं और अपने जीवन जीती हैं। आज हम "भविष्यवाणी" और "अपमानजनक" का उपयोग करने के तरीके काफी अलग हैं, क्योंकि जिन चीजों के बारे में हम चिंतित हैं, वे बदल गए हैं। तो कभी-कभी यह देखने में थोड़ा मुश्किल हो सकता है कि हमारे आधुनिक उपयोग की बिल्ली कैसे इस सामान से जुड़ी हुई है। ईमानदारी से, मुझे नहीं लगता कि व्युत्पत्ति विज्ञान वास्तव में किसी भी चीज को जानने में मदद करता है कि वास्तव में शब्द क्या हैं (इन दिनों)।
यहां उस ऐतिहासिक संदर्भ के लिए धन्यवाद। बहुत सराहना की! – sclv
तो, कुछ लक्स प्रतिबंध 'आर' के लिए, यह हमें स्थिरता के मामले में' आर '-पूर्वानुमानक होने के लिए बहुत कुछ नहीं खरीदता है, है ना? उस अर्थ में 'भविष्यवाणी' स्थिरता को इंगित नहीं करता है, जैसा कि 'विरोधाभासी मुक्त' में है, अगर मुझे गलत नहीं लगता है ... –
किसी भी प्रकार की अच्छी शर्तों नहीं हैं 'forall a। ए', लेकिन बहुत समझदार polymorphic शर्तों हैं। मुझे नहीं लगता कि मैं क्यों नहीं चाहता * उन * ... – dfeuer
@ डीफ्यूअर हाँ, वहां बहुत समझदार पॉलीमोर्फिक शब्द हैं। लेकिन (एक अनुमानित प्रणाली में) ऐसे कोई भी शब्द नहीं हैं जिनके प्रकार पॉलिमॉर्फिक तत्व प्रकार के साथ एक सूची है, इससे कोई फर्क नहीं पड़ता कि आप कौन सी पॉलिमॉर्फिक तत्व प्रकार चुनते हैं! –
@DanielWagner, आह, मुझे लगता है कि मैं देखता हूं कि अब आप क्या मतलब है। – dfeuer