एक पूर्ण प्रकार की अनुमानित भाषा क्या है? और ऐसी भाषा की सीमाएं?

Question

जहां तक ​​मुझे पता है, किसी भी प्रोग्रामिंग भाषा को फ़ंक्शन या मॉड्यूल लिखते समय स्रोत में टाइप एनोटेशन लिखने की आवश्यकता नहीं होती है और यदि कोड का वह हिस्सा "टाइप-सही" है, तो कंपाइलर प्रकारों का अनुमान लगाएगा और संकलित करेगा कोड। इसके लिए और कुछ है?

ऐसी भाषाएं हैं (ओं) हैं? यदि हां इसके प्रकार की प्रणाली पर कोई सीमाएं हैं?

अद्यतन 1: बस होने के लिए वास्तव में स्पष्ट, मैं एक स्थिर टाइप किया, पूरी तरह से टाइप-inferred प्रोग्रामिंग भाषा नहीं एक गतिशील टाइप किया प्रोग्रामिंग भाषा के बारे में पूछ रहा हूँ।

Answer 1

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

---

हास्केल में यह के प्रकार बहुरूपी वापसी प्रकार के साथ संयुक्त कक्षाएं:

readAndPrint str = print (read "asd") 

यहाँ read प्रकार Read a => String -> a के एक समारोह है, जो "किसी भी प्रकार a कि प्रकार वर्ग Read समारोह का समर्थन करता है के लिए इसका मतलब है readString ले सकते हैं और a वापस कर सकते हैं। इसलिए यदि f एक तरीका है जो एक int लेता है, तो मैं f (read "123") लिख सकता हूं और यह "123" को Int 123 में परिवर्तित कर देगा और f पर कॉल करेगा यह। यह जानता है कि इसे स्ट्रिंग को int में परिवर्तित करना चाहिए क्योंकि f एक इंट लेता है। अगर एफ ने इन्ट्स की एक सूची ली है, तो यह स्ट्रिंग को इंट्स की सूची में बदलने की कोशिश करेगा। कोई बात नहीं।

लेकिन उस दृष्टिकोण के ऊपर readAndPrint फ़ंक्शन के लिए काम नहीं करता है। यहां समस्या यह है कि print किसी भी प्रकार का तर्क ले सकता है जिसे मुद्रित किया जा सकता है (यह कोई भी प्रकार है जो Show टाइपक्लास का समर्थन करता है)। तो संकलक के बारे में जानने का कोई तरीका नहीं है कि क्या आप स्ट्रिंग को एक int, या ints की सूची में परिवर्तित करना चाहते हैं, या मुद्रित किए जा सकने वाले किसी और चीज को बदलना चाहते हैं। तो इस तरह के मामलों में आपको टाइप एनोटेशन जोड़ने की जरूरत है।

---

OCaml में समस्याग्रस्त सुविधा कक्षाओं में बहुरूपी कार्यों है: यदि आप एक समारोह है कि उस वस्तु पर अपने तर्क के रूप में एक वस्तु लेता है और एक प्रणाली को बुलाती है निर्धारित करते हैं संकलक कि विधि के लिए एक monomorphic प्रकार का अनुमान लगा होगा। उदाहरण के लिए:

let f obj = obj#meth 23 + obj#meth 42 

यहाँ संकलक का अनुमान लगा होगा कि obj एक वर्ग एक विधि प्रकार int -> int की meth नाम है, अर्थात एक विधि है कि एक इंट लेता है और एक इंट देता है का एक उदाहरण होना चाहिए। अब आप कक्षाओं का एक गुच्छा परिभाषित कर सकते हैं जिसमें f पर तर्क के रूप में उस वर्ग की ऐसी विधि और पास उदाहरण हैं। कोई बात नहीं।

समस्या तब होती है जब आप 'a. 'a -> int प्रकार की विधि के साथ कक्षा को परिभाषित करते हैं, यानी कोई तरीका जो किसी भी प्रकार का तर्क ले सकता है और एक int वापस कर सकता है। आप f पर तर्क के रूप में उस वर्ग की किसी ऑब्जेक्ट को पास नहीं कर सकते क्योंकि यह अनुमानित प्रकार से मेल नहीं खाता है। यदि आप f चाहते हैं तो इस तरह के ऑब्जेक्ट को इसके तर्क के रूप में लेने के लिए, एकमात्र तरीका f पर एक प्रकार की एनोटेशन जोड़ना है।

---

तो वे उन भाषाओं के उदाहरण थे जो अनुमानित रूप से अनुमानित रूप से अनुमानित हैं और जिन मामलों में वे नहीं हैं। यदि आप उन भाषाओं से समस्याग्रस्त विशेषताओं को हटा देंगे, तो वे पूरी तरह से अनुमानित प्रकार का अनुमान लगाएंगे।

परिणामस्वरूप एमएल के मूलभूत बोली ऐसी उन्नत सुविधाओं के बिना पूरी तरह से अनुमानित हैं। उदाहरण के लिए मुझे लगता है कि कैमल लाइट पूरी तरह से अनुमानित है क्योंकि यह कक्षाओं के बिना मूल रूप से ओकैमल है (हालांकि मुझे वास्तव में भाषा नहीं पता है, इसलिए यह केवल एक धारणा है)।

Answer 2

प्रकार अनुमान क्या है?

ऐतिहासिक रूप से, प्रकार निष्कर्ष (या प्रकार पुनर्निर्माण) का मतलब है कि एक कार्यक्रम में सभी प्रकार अनिवार्य रूप से किसी भी स्पष्ट प्रकार एनोटेशन की आवश्यकता के बिना प्राप्त किया जा सकता। हालांकि, हाल के वर्षों में, यह प्रोग्रामिंग भाषा मुख्यधारा में "प्रकार अनुमान" के रूप में नीचे-प्रकार के प्रकार के कटौती के सबसे छोटे रूपों को लेबल करने के लिए प्रचलित हो गया है (उदाहरण के लिए, नई auto सी ++ 11 की घोषणा)। इसलिए लोगों ने "वास्तविक" चीज़ को संदर्भित करने के लिए "पूर्ण" जोड़ना शुरू कर दिया है।

पूर्ण प्रकार अनुमान है?

एक व्यापक स्पेक्ट्रम है कि एक भाषा किस प्रकार की भाषा का अनुमान लगा सकती है, और व्यावहारिक रूप से, लगभग कोई भी भाषा सख्ती से समझ में "पूर्ण" प्रकार अनुमान का समर्थन नहीं करती है (कोर एमएल एकमात्र उदाहरण है)। लेकिन मुख्य विशिष्ट कारक यह है कि क्या प्रकार बाइंडिंग के लिए प्राप्त किए जा सकते हैं जिनके पास विशेष रूप से — से जुड़ी "परिभाषा" नहीं है, कार्यों के पैरामीटर। यदि आप लिख सकते हैं, कहें,

f(x) = x + 1 

और टाइप सिस्टम उस एफ को बताता है उदा। इंट → इंट टाइप किया गया है, तो इस प्रकार की अनुमान को कॉल करना समझ में आता है। (टी) टी → स्वचालित रूप से; इसके अलावा, हम के बारे में बहुरूपी प्रकार निष्कर्ष जब बात करते हैं, उदाहरण के लिए,

g(x) = x 

सामान्य प्रकार & forall असाइन किया गया है।

टाइप अनुमान का आविष्कार आसानी से टाइप किए गए लैम्ब्डा कैलकुस के संदर्भ में किया गया था, और पॉलिमॉर्फिक प्रकार अनुमान (उर्फ हिंडली/मिलनर प्रकार अनुमान, 1 9 70 के दशक में आविष्कार) एमएल परिवार के भाषाओं की प्रसिद्धि का दावा है (मानक एमएल , ओकैमल, और तर्कसंगत हास्केल)।

पूर्ण प्रकार की अनुमान की सीमाएं क्या हैं?

कोर एमएल में "पूर्ण" पॉलिमॉर्फिक प्रकार अनुमान की लक्जरी है। लेकिन यह अपने प्रकार के सिस्टम में बहुरूपता की कुछ सीमाओं पर निर्भर करता है। विशेष रूप से, केवल परिभाषाएं सामान्य हो सकती हैं, कार्य तर्क नहीं। यही है,

id(x) = x; 
id(5); 
id(True) 

ठीक काम करता है, क्योंकि id बहुरूपी प्रकार दिया जा सकता है जब परिभाषा जाना जाता है। लेकिन

f(id) = (id(5); id(True)) 

प्रकार एमएल में जांच नहीं करता, क्योंकि id एक समारोह तर्क के रूप में बहुरूपी नहीं हो सकता।दूसरे शब्दों में, टाइप सिस्टम पॉलिमॉर्फिक प्रकारों को और इसके लिए अनुमति देता है; (टी) टी → टी, लेकिन तथाकथित उच्च-रैंक पॉलिमॉर्फिक प्रकार (& forall; (टी) टी → टी) → बूल, जहां पॉलिमॉर्फिक मानों का उपयोग किया जाता है एक प्रथम श्रेणी के तरीके में (जो, स्पष्ट होने के लिए, यहां तक ​​कि बहुत कम स्पष्ट रूप से टाइप की जाने वाली भाषाएं भी अनुमति देते हैं)।

पॉलिमॉर्फिक लैम्ब्डा कैलकुस (जिसे "सिस्टम एफ" भी कहा जाता है), जिसे स्पष्ट रूप से टाइप किया गया है, बाद वाले को अनुमति देता है। लेकिन यह एक मानक परिणाम प्रकार सिद्धांत में है जो पूर्ण सिस्टम एफ के लिए पुनर्निर्माण टाइप अपरिहार्य है। हिंडली/मिलनर थोड़ा कम अभिव्यक्तिपूर्ण प्रकार प्रणाली का मीठा स्थान हिट करता है जिसके लिए पुनर्निर्माण अभी भी निर्णायक है।

अधिक उन्नत प्रकार की सिस्टम विशेषताएं हैं जो पूर्ण प्रकार के पुनर्निर्माण को भी निर्विवाद बनाती हैं। और ऐसे कुछ भी हैं जो इसे निर्णायक रखते हैं लेकिन फिर भी इसे अक्षम बनाते हैं, उदा। विज्ञापन-हाक ओवरलोडिंग या सबटाइपिंग की उपस्थिति, क्योंकि इससे संयोजक विस्फोट होता है।

Answer 3

एक और सीमा उच्च रैंक प्रकार हैं। उदाहरण के लिए, निम्नलिखित कार्यक्रम एमएल शैली प्रकार निष्कर्ष के साथ भाषाओं में नहीं typecheck करता है:

foo = let bar f = (f ['a', 'b', 'c'], f [1,2,3]) in bar reverse 

प्रकार चेकर को असाइन कर सकते प्रकार [चार] च -> [चार] या [इंट] -> [Int], लेकिन कुल मिलाकर नहीं। [ए] -> [ए]। एमएल, ओकैम और एफ # में इसे ठीक करने का कोई तरीका नहीं है, क्योंकि आप उच्च रैंक प्रकार भी लिख नहीं सकते हैं।

लेकिन हास्केल (एक जीएचसी एक्सटेंशन के माध्यम से) और फ्रीज उच्च रैंक प्रकार का समर्थन करते हैं। लेकिन क्योंकि केवल उच्च पद प्रकार (के रूप में उच्च पद प्रकार निष्कर्ष के खिलाफ) की जाँच के लिए संभव है, प्रोग्रामर उदाहरण के लिए, एक प्रकार एनोटेशन देने के लिए, हालांकि आवश्यक है:

foo = let bar (f :: forall a.[a]->[a]) = (f ['a', 'b', 'c'], f [1,2,3]) in bar reverse