2008-09-07 26 views
14

मैं हास्केल के बारे में एक शोध पत्र पढ़ रहा था और एचएलिस्ट कैसे कार्यान्वित किया गया था और सोच रहा था कि जब वर्णित तकनीकें प्रकार के चेकर के लिए निर्णायक नहीं हैं। इसके अलावा, क्योंकि आप जीएडीटी के साथ समान चीजें कर सकते हैं, मैं सोच रहा था कि क्या जीएडीटी प्रकार की जांच हमेशा निर्णायक है।फंडप और जीएडीटी: टाइपिंग की जांच कब की जा सकती है?

यदि आपके पास है तो मैं उद्धरण पसंद करूंगा ताकि मैं स्पष्टीकरण को पढ़/समझ सकूं।

धन्यवाद!

+1

यह प्रश्न शोध पत्र के लेखकों को बेहतर निर्देशित किया जा सकता है। यह स्टैक ओवरफ़्लो के लिए थोड़ा गूढ़ है। (मुझे हमेशा टिप्पणी के लिए शोधकर्ताओं से संपर्क करने में बड़ी सफलता मिली है। वे आमतौर पर उत्साही होते हैं * कोई भी * अपना काम पढ़ रहा है।) –

+7

मुझे लगता है कि यह रवैया (सैद्धांतिक प्रश्नों को व्यावहारिक मंच पर कोई असर नहीं है) हानिकारक और अप्रचलित है। व्यावहारिक दृष्टिकोण नई प्रौद्योगिकियों के लिए खुले रहना चाहिए, क्योंकि उन प्रौद्योगिकियों के निकट भविष्य में दैनिक गतिविधियों में सुधार हो सकता है। उदाहरण: सी #/पायथन में कार्यात्मक विशेषताएं। – rcreswick

+0

उस ने कहा, चीर्स की टिप्पणी शायद व्यावहारिक रूप से बोल रही है। मेरी इच्छा है कि यह नहीं था। – rcreswick

उत्तर

8

मुझे विश्वास है कि जीएडीटी प्रकार की जांच हमेशा निर्णायक है; यह अनुमान है जो अपरिहार्य है, क्योंकि इसे उच्च आदेश एकीकरण की आवश्यकता है। लेकिन एक जीएडीटी प्रकार चेकर उदाहरण में उदाहरण प्रूफ चेकर्स का एक प्रतिबंधित रूप है। Coq, जहां रचनाकार सबूत अवधि का निर्माण। उदाहरण के लिए, जीएडीटी में लैम्ब्डा कैलकुस को एम्बेड करने का क्लासिक उदाहरण प्रत्येक कमी नियम के लिए एक कन्स्ट्रक्टर है, इसलिए यदि आप किसी शब्द का सामान्य रूप ढूंढना चाहते हैं, तो आपको यह बताना होगा कि कौन से निर्माता आपको प्राप्त करेंगे। रोक समस्या को उपयोगकर्ता के हाथों में स्थानांतरित कर दिया गया है :-)

+0

यह एक अच्छा मुद्दा है। तो मुझे लगता है कि मुझे इसमें दिलचस्पी है जब जीएडीसी के जीएडीटी के प्रकार का अनुमान निर्णायक है। –

1

आपने शायद इसे पहले ही देखा है लेकिन माइक्रोसॉफ्ट रिसर्च में इस मुद्दे पर कागजात का संग्रह है: Type Checking papers। पहला ग्लासगो हास्केल कंपाइलर में वास्तव में उपयोग किए जाने वाले निर्णायक एल्गोरिदम का वर्णन करता है।

+0

संदर्भित कागजात अच्छे कागजात हैं, लेकिन वे मेरे प्रश्न का उत्तर नहीं देते हैं। –