जीएचसी के मामलों में पहचान के मामले क्या होते हैं?

Question

जीएचसी होता है चेक आपको अनंत प्रकार के निर्माण से रोकता है। क्या कोड में सामान्य त्रुटियों को रोकने या टाइपशेकर को अनिश्चित काल तक लूप करने से रोकने का उद्देश्य है, या दोनों?

यह कौन सा मामला पहचानता है और क्या यह दुर्भावनापूर्ण उपयोगकर्ता को लूपिंग में (जैसे एक सुरक्षित हास्केल संदर्भ में) चालित करना संभव है? यदि टाइप सिस्टम पूरा हो रहा है (है ना?) मुझे समझ में नहीं आता कि जीएचसी कैसे गारंटी दे सकता है कि गणना रोक दी जाएगी।

Answer 1

समीकरणों की एक प्रणाली को हल करने के प्रकार प्रकार अनुमान के बारे में सोचें। चलो एक उदाहरण देखते हैं:

f x = (x,2) 

हम f के प्रकार कैसे मान सकते हैं? हम देखते हैं कि यह एक समारोह है:

f :: a -> b 

साथ ही, f की संरचना से हम देख सकते हैं कि निम्नलिखित समीकरणों simulatenously पकड़:

b = (c,d) 
d = Int 
c = a 

समीकरणों की इस प्रणाली हम देख सकते हैं कि सुलझाने तक f का प्रकार a -> (a, Int) है। अब हम निम्नलिखित (गलत) समारोह को देखो:

f x = x : x 

(:) के प्रकार a -> [a] -> [a] है, इसलिए इस समीकरणों के निम्नलिखित प्रणाली (सरलीकृत) उत्पन्न करता है:

a = a 
a = [a] 

तो हम एक समीकरण मिल a = [a], जिसमें से हम निष्कर्ष निकाल सकते हैं कि समीकरणों की इस प्रणाली में कोई समाधान नहीं है, और इसलिए कोड अच्छी तरह से टाइप नहीं किया गया है। अगर हमने समीकरण a = [a] को अस्वीकार नहीं किया है, तो हम वास्तव में एक अनंत लूप को समीकरण a = [a], a = [[a]], a = [[[a]]], आदि हमारे सिस्टम में (वैकल्पिक रूप से, डैनियल नोट्स के उत्तर में, हमारे प्रकार के सिस्टम में अनंत प्रकारों की अनुमति दे सकते हैं, लेकिन यह टाइपशेक के लिए f x = x : x जैसे गलत प्रोग्राम करेगा)।

तुम भी GHCi में इस परीक्षण कर सकते हैं:

> let f x = x : x 

<interactive>:2:15: 
    Occurs check: cannot construct the infinite type: a0 = [a0] 
    In the second argument of `(:)', namely `x' 
    In the expression: x : x 
    In an equation for `f': f x = x : x 

अपने अन्य सवाल के रूप में: GHC हास्केल के प्रकार प्रणाली ट्यूरिंग-पूर्ण नहीं है और typechecker को रोकने के लिए गारंटी है - जब तक आप UndecidableInstances सक्षम, जिस स्थिति में यह सैद्धांतिक रूप से एक अनंत पाश में जा सकते हैं। हालांकि, जीएचसी एक निश्चित गहराई से रिकर्सन स्टैक, होने से समाप्त होने को सुनिश्चित करता है, इसलिए यह प्रोग्राम बनाना संभव नहीं है जिस पर यह कभी भी (संपादित नहीं करता है: सीएएमसीकैन की टिप्पणी के अनुसार, यह सब संभव है - एक एनालॉग है प्रकार के स्तर पर पूंछ रिकर्सन की जो स्टैक गहराई को बढ़ाए बिना लूप की अनुमति देता है)।

हालांकि, संकलन को मनमाने ढंग से लंबे समय तक लेना संभव है, क्योंकि हिंडली-मिलनर प्रकार की अनुमान की जटिलता सबसे बुरी स्थिति में घातीय है (लेकिन औसत नहीं!) मामला:

dup x = (x,x) 

bad = dup . dup . dup . dup . dup . dup . dup . dup 
     . dup . dup . dup . dup . dup . dup . dup . dup 
     . dup . dup . dup . dup . dup . dup . dup . dup 
     . dup . dup . dup . dup . dup . dup . dup . dup 

सुरक्षित हास्केल इस से बचाने नहीं होगा - mueval पर एक नज़र डालें यदि आप संभावित रूप से दुर्भावनापूर्ण उपयोगकर्ताओं को अपने सिस्टम पर हास्केल कार्यक्रमों संकलन अनुमति देना चाहते हैं।

Answer 2

मेरे पास मेरे बुकमार्क में निम्नलिखित अद्भुत मेल है: There's nothing wrong with infinite types! असीमित प्रकारों के साथ भी, टाइपशेकर लूप बनाने का कोई वास्तविक खतरा नहीं है। टाइप सिस्टम ट्यूरिंग पूर्ण नहीं है (जब तक कि आप इसे स्पष्ट रूप से UndecidableInstances एक्सटेंशन जैसे कुछ के साथ न पूछें)।

Answer 3

जीएचसी होता है चेक आपको अनंत प्रकार के निर्माण से रोकता है।

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

रिकर्सन स्पष्ट करके बिल्कुल उसी प्रकार को परिभाषित करना हमेशा संभव है। यह भी सामान्य रूप से किया जा सकता है, fix का एक प्रकार स्तरीय संस्करण का उपयोग कर:

newtype Fix f = Fix (f (Fix f)) 

उदाहरण के लिए, प्रकार Fix ((->) a)(a -> b) साथ एकीकृत b के बराबर है।

अभ्यास में, हालांकि, "अनंत प्रकार" त्रुटियां लगभग हमेशा कोड में एक त्रुटि इंगित करती हैं (इसलिए यदि यह तोड़ दिया गया है, तो आपको शायद Fix नहीं होना चाहिए)। सामान्य परिदृश्य तर्क आदेश को मिश्रित कर रहा है या अन्यथा कोड में गलत जगह में अभिव्यक्ति है जो स्पष्ट प्रकार हस्ताक्षर का उपयोग नहीं करता है।

एक प्रकार की अनुमान प्रणाली जो कि सही तरीके से बेहद बेवकूफ़ थी, संभवत: स्मृति से बाहर होने तक रिकर्सन का विस्तार कर सकती है, लेकिन रोकथाम की समस्या इसमें प्रवेश नहीं करती है - अगर किसी प्रकार को स्वयं के हिस्से के साथ एकजुट होना चाहिए , यह कभी भी काम नहीं करेगा (कम से कम हास्केल में, ऐसी भाषाएं हो सकती हैं जो इसके बजाय इसे स्पष्ट रूप से रिकर्सिव newtype के बराबर मानती हैं)।

जीएचसी में कोई भी प्रकार की जांच न करें और टाइप करें, जब तक आप UndecidableInstances सक्षम नहीं करते हैं, तब तक आप कार्यशील निर्भरताओं या परिवारों के प्रकार के माध्यम से मनमाने ढंग से गणना कर सकते हैं।

सुरक्षित हास्केल वास्तव में तस्वीर में प्रवेश नहीं करता है। बहुत बड़े अनुमानित प्रकार उत्पन्न करना आसान है जो सीमित होने के बावजूद सिस्टम मेमोरी को समाप्त कर देंगे, और यदि स्मृति मुझे सेवा प्रदान करती है तो सुरक्षित हास्केल UndecidableInstances के उपयोग को प्रतिबंधित नहीं करता है।

Answer 4

उद्देश्य (हास्केल कंपाइलर्स में) कोड में सामान्य त्रुटियों को रोकने के लिए है। एक प्रकार का चेकर और अनुमान इंजन बनाना संभव है जो प्रकारों के अनंत रिकर्सन का समर्थन करेगा। this question में कुछ और जानकारी है।

ओकैमल -rectypes के साथ पुनरावर्ती प्रकार लागू करता है, इसलिए यह निश्चित रूप से संभव है। OCaml समुदाय उत्पन्न होने वाली कुछ समस्याओं में बहुत अधिक जानकारी प्राप्त करेगा (व्यवहार डिफ़ॉल्ट रूप से बंद है)।

होता है चेक असीमित प्रकार के विस्तार की पहचान करता है। उदाहरण के लिए, इस कोड:

Prelude> let a = [a] 
<interactive>:2:10: 
    Occurs check: cannot construct the infinite type: t0 = [t0] 
    In the expression: a 
    In the expression: [a] 
    In an equation for `a': a = [a] 

अगर आप हाथ से टाइप बाहर काम करने की कोशिश, प्रकार [ [ [ [ ... ] ] ] ] है। हाथों से ऐसे प्रकार लिखना असंभव है, क्योंकि वे अनंत हैं।

होता है चेक प्रकार संदर्भ के दौरान होता है, जो प्रकार की जांच से एक अलग चरण है।अनंत प्रकारों को अनुमानित किया जाना चाहिए, क्योंकि उन्हें मैन्युअल रूप से एनोटेट नहीं किया जा सकता है। हास्केल -98 प्रकार अनुमान decidable है, इसलिए संकलक को लूपिंग में घुमाने के लिए असंभव है (निश्चित रूप से बग को छोड़कर, जिसे मुझे this example शोषण पर संदेह है)। डिफ़ॉल्ट रूप से जीएचसी सिस्टम एफ के प्रतिबंधित सबसेट का उपयोग करता है जिसके लिए प्रकार अनुमान भी decidable है। कुछ एक्सटेंशन के साथ, जैसे कि RankNTypes, जीएचसी कोड को अनुमति देता है कि किस प्रकार के अनुमान को अपरिहार्य है, लेकिन फिर एक प्रकार की एनोटेशन की आवश्यकता होती है, इसलिए फिर प्रकार अनुमान लूपिंग प्रकार का कोई खतरा नहीं है।

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

संयोग से, अक्षम करने से होता है की जांच के साथ मुख्य समस्या यह है कि कई आम कोडिंग गलतियों अनंत प्रकार त्रुटियों में परिणाम है, इसलिए इसे अक्षम करना आम तौर पर और अधिक समस्याओं की ओर जाता है की तुलना में यह हल करती है। यदि आप एक अनंत प्रकार का उपयोग करने का इरादा रखते हैं, तो एक नया टाइपर इसे बिना किसी अतिरिक्त नोटेशन के अनुमति देगा।