कौन सा विश्वसनीय रूप से टाइप किया गया प्रोग्रामिंग भाषाओं का उपयोग वास्तविक विश्व अनुप्रयोग विकास के लिए किया जा सकता है?निर्भर रूप से टाइप की गई भाषा "असली दुनिया" प्रोग्रामिंग के लिए सबसे उपयुक्त है?
ये कुछ बातें बताई गई हैं मुझे लगता है कि महत्वपूर्ण हैं कि:
मैं Agda का सुझाव दूंगा, क्योंकि यह हास्केल के साथ संगतता को कॉल कर रहा है। इस प्रकार, यह शायद सर्वश्रेष्ठ पुस्तकालयों के साथ निर्भर रूप से टाइप की गई भाषा है। हालांकि दस्तावेज़ीकरण और ट्यूटोरियल थोड़ा कमजोर हैं, और टूल समर्थन भी बहुत अच्छा नहीं है। ईमानदार होने के लिए, इस समय सबसे अधिक निर्भर रूप से टाइप की गई भाषाएं पूरी तरह से विकसित नहीं हुई हैं।
यदि आप थोड़ी कमजोर मांग के साथ गए थे कि आपकी भाषा में GADT's हो, तो दो बहुत अच्छी तरह से बनाए रखा विकल्प हैं: स्कैला और हास्केल। आईएमएचओ आपको जीएडीटी का उपयोग करके निर्भर प्रकारों के अधिकांश लाभ मिलते हैं, और आप बूट करने के लिए निर्णायक टाइपशेकिंग रखते हैं।
स्कैला और हास्केल दोनों में बड़ी और अच्छी तरह से प्रलेखित पुस्तकालय, एक कार्यरत उपकरण श्रृंखला, साथ ही एफएफआई (जावा और सी क्रमशः) हैं। दोनों भी उन्हें प्रयोग वास्तविक दुनिया की समस्याओं को हल करने के parsing और webdevelopment.
मैं थोड़ी देर के लिए स्कैला का उपयोग कर रहा हूं, लेकिन मैंने जीएडीटी का उपयोग नहीं किया है। वे निर्भर प्रकार से कैसे संबंधित हैं? –
जीएडीटी निर्भर प्रकारों और नियमित पैरामीट्रिक प्रकारों के बीच एक उपयोगी मध्यवर्ती कदम है। आपको अधिकांश प्रकार की प्रणालियों की तुलना में मजबूत टाइपिंग मिलती है, और एक प्रकार की प्रणाली होने से कम रुकती है जो निर्भर टाइपिंग की तरह पूर्ण (अनावश्यक) ट्यूरिंग कर रही है। एक अनावश्यक प्रकार प्रणाली को रोकना थोड़ा समस्याग्रस्त है क्योंकि टाइप-चेकिंग में अनिश्चित काल तक लूप करने का एक छोटा सा मौका है। इसलिए जब तक आपको पता न हो कि आपको निर्भर टाइपिंग से अतिरिक्त प्रकार की जानकारी की आवश्यकता होगी तो आप जीएडीटी पर रोक लगाने से बेहतर हो सकते हैं। क्योंकि वे आपको अभी भी निर्णायक होने के दौरान अधिकांश प्रकार की प्रणालियों की तुलना में कूलर चीजें करने की अनुमति देते हैं। – keiter
संदर्भ के लिए, ओकैमल अब भी जीएडीटी का समर्थन करता है। –
AGDA की तरह एक सामान्य प्रयोजन प्रोग्रामिंग भाषा नहीं बनाया गया है समुदायों की है। एटीएस एक निर्भर रूप से टाइप की गई भाषा है जो निम्न स्तर के प्रोग्रामिंग के लिए डिज़ाइन की गई है, हालांकि यह एजडा से कुछ हद तक कम सुरुचिपूर्ण है। इडिस प्रदर्शनकारी अनुप्रयोग-स्तर के कार्यक्रमों के लिए डिज़ाइन की गई एक अविश्वसनीय रूप से टाइप की गई भाषा है।
स्वीकृत उत्तर में गलत जानकारी है। Agda में टाइपशेकिंग निर्णायक है जब तक आप सकारात्मकता/समाप्ति/ब्रह्मांड जांच बंद नहीं करते हैं। इसके अलावा, अनंत प्रक्रियाएं एग्डा में प्रोग्राम करने योग्य हैं, जैसे आईओ प्रक्रियाएं हास्केल में प्रोग्राम करने योग्य हैं: केवल प्रतिबंध यह है कि टाइपशेकिंग के दौरान निष्पादित होने पर अनंत प्रक्रियाओं को अनिश्चित काल तक प्रकट नहीं किया जा सकता है। आप एग्डा में ट्यूरिंग मशीन सिम्युलेटर को कार्यान्वित कर सकते हैं: आप सिर्फ झूठ को नहीं बता सकते हैं कि इसे टाइपशेकर को बिना किसी घुमावदार तरीके से चलाने के लिए समाप्त करने या मनाने के लिए गारंटी दी गई है।
हालांकि, मैं सहमत हूं कि "वास्तविक दुनिया" प्रोग्रामिंग की बात आती है जब निर्भर रूप से टाइप की गई भाषाएं प्रयोगात्मक चरण में हैं। हम अभी तक भारी कर्तव्य विकास का समर्थन नहीं कर सकते हैं, लेकिन हम पुराने दिनों में कार्यात्मक भाषाओं की तरह भविष्य में नजर रखने वाले लोगों के बीच एक महत्वपूर्ण शौक बनाए रख सकते हैं।
ट्री द्वारा सुझाए गए इडिस, "असली दुनिया" पर निर्भर रूप से टाइप की गई भाषा के निकटतम उम्मीदवार हैं। एजडा की तुलना में सामान प्राप्त करने पर यह बहुत अधिक केंद्रित है। मैं एग्डा को निर्भर रूप से टाइप किए गए प्रोग्रामिंग के पीछे विचारों के साथ पकड़ने के लिए बेहतर वाहन के रूप में अनुशंसा करता हूं, लेकिन इडिस अधिक व्यावहारिक विकल्प है।
यह है, मैं इस चर्चा में उम्मीदवार के रूप में हास्केल की हालिया रिलीज पर विचार करने के लायक हूं। जीएचसी 7 के बाद से।4, हास्केल ने टाइप लेवल डेटा की एक उपयोगी धारणा का समर्थन करना शुरू कर दिया है, और कम से कम सिंगलटन तकनीक (हालांकि यह एक क्लज है) के साथ, हम वास्तव में रन-टाइम मानों के आधार पर प्रकार प्राप्त कर सकते हैं (उन्हें स्थिर चर पर निर्भर करते हुए बराबर रन-टाइम मानों तक सीमित)। हास्केल आश्रित प्रकारों के प्रयोग के शुरुआती चरण में वास्तविक "वास्तविक दुनिया" भाषा है।
उत्तर के लिए धन्यवाद। हास्केल की क्षमताओं कितनी दूर जाती है? ऐसा लगता है कि यह इस संबंध में स्काला से तुलनीय है। –
मुझे नहीं लगता कि स्कैला उस तुलना में काफी अच्छा है। हालांकि, हास्केल निर्भर रूप से टाइप की गई दिशा में काफी गति से आगे बढ़ रहा है। दयालु बहुरूपता (जैसा कि जीएचसी 7.6 में) प्रकार को स्वचालित रूप से प्रकार के स्तर पर प्रचारित करके बनाए गए सभी नए प्रकारों के साथ प्रभावी ढंग से काम करना संभव बनाता है। मेरी शर्त हास्केल पर होगी और इस सम्मान में स्कैला से आगे रहती है, लेकिन मुझे गलत साबित होने में खुशी होगी। – pigworker
एर, उम, मुझे यह बताएं कि मेरे आईसीएफपी2012 टॉक से विकास https://t.co/fB8sFizL http://www.youtube.com/watch?v=XGyJ519RY6Y धीरे-धीरे अधिक निर्भर रूप से टाइप करने में एक अभ्यास है। हास्केल आसानी से भाग 4 के लिए सभी तरह से मिल सकता है, लेकिन भाग 5 के लिए उम्मीद करने के लिए बहुत अधिक है। क्या संभव है इसके उदाहरण के लिए http://stackoverflow.com/questions/10656402/is-it-possible-to-program-and-check-invariants-in-haskell/10659438#10659438 भी देखें। – pigworker
प्रोग्रामर.स्टैकएक्सchange.com के लिए बेहतर फिट हो सकता है ... – ChristopheD
उनमें से कोई भी इस्तेमाल किया जा सकता है। आपको अपने प्रश्न के लिए अधिक संदर्भ प्रदान करने की आवश्यकता है। – jzd
पूर्णता ट्यूरिंग के बारे में क्या? क्या यह भी एक आवश्यकता है? इसके अलावा जब आप "असली दुनिया के कार्यों" कहते हैं, तो आपका मतलब है "विकासशील अनुप्रयोग" - "प्रमेय सिद्ध करना" नहीं, है ना? – sepp2k