रैंक-एन प्रकारों का सबसे हालिया प्रस्ताव डॉन के लिंक किए गए एफपीएच पेपर है। मेरी राय में यह गुच्छा का सबसे अच्छा भी है। इन सभी प्रणालियों का मुख्य लक्ष्य जितना संभव हो उतना प्रकार के एनोटेशन की आवश्यकता है। समस्या यह है कि जब हिंडली/मिलनर से सिस्टम एफ तक जा रहे हैं तो हम मूल प्रकार खो देते हैं और टाइप अनुमान अनुमानित हो जाता है - इसलिए एनोटेशन टाइप करने की आवश्यकता होती है।
"बॉक्सी प्रकार" काम का मूल विचार टाइप एनोटेशन को यथासंभव प्रचारित करना है। टाइप चेकर प्रकार की जांच और टाइप अनुमान मोड के बीच स्विच करता है और उम्मीद है कि कोई और एनोटेशन की आवश्यकता नहीं है। यहां नकारात्मकता यह है कि एक प्रकार की एनोटेशन की आवश्यकता है या नहीं, यह समझाना मुश्किल है क्योंकि यह कार्यान्वयन के विवरण पर निर्भर करता है।
रेमी का एमएलएफ सिस्टम अब तक का सबसे अच्छा प्रस्ताव है; इसे कम से कम प्रकार की एनोटेशन की आवश्यकता होती है और कई कोड ट्रांसफॉर्मेशन के तहत स्थिर होती है। समस्या यह है कि यह प्रकार प्रणाली को बढ़ाता है। निम्न मानक उदाहरण इस दिखाता है:
choose :: forall a. a -> a -> a
id :: forall b. b -> b
choose id :: forall c. (c -> c) -> (c -> c)
choose id :: (forall c. c -> c) -> (forall c. c -> c)
उपरोक्त दोनों प्रकार के सिस्टम एफ में admissable पहले एक मानक Hindley/मिलनर प्रकार है और प्रेडीकेटिव इन्स्टेन्शियशन का उपयोग करता है, दूसरा एक impredicative इन्स्टेन्शियशन उपयोग करता है। न तो प्रकार दूसरे की तुलना में अधिक सामान्य है, इसलिए अनुमान लगाएं कि उपयोगकर्ता किस प्रकार का चाहता है, और यह आमतौर पर एक बुरा विचार है।
एमएलएफ इसके बजाय सिस्टम एफ को बाध्य मात्रा के साथ बढ़ाता है।प्रिंसिपल (= सबसे सामान्य) ऊपर के उदाहरण के लिए टाइप होगा:
choose id :: forall (a < forall b. b -> b). a -> a
आप के रूप में इस पढ़ें "choose id टाइप है aa जहां aforall b. b -> b का एक उदाहरण होना चाहिए करने के लिए" कर सकते हैं।
दिलचस्प बात यह है कि यह अकेले मानक हिंडली/मिलनर से अधिक शक्तिशाली नहीं है। एमएलएफ इसलिए कठोर मात्रा को भी अनुमति देता है। निम्नलिखित दो प्रकार के बराबर हैं:
(forall b. b -> b) -> (forall b. b -> b)
forall (a = forall b. b -> b). a -> a
कठोर मात्रा प्रकार एनोटेशन और तकनीकी जानकारी से शुरू की है वास्तव में बहुत जटिल हैं। उलझन यह है कि एमएलएफ को केवल बहुत कम प्रकार की टिप्पणियों की आवश्यकता होती है और जब उनकी आवश्यकता होती है तो उनके लिए एक सरल नियम होता है। कमियां हैं:
प्रकार, पढ़ने के लिए कठिन हो सकता है, क्योंकि '<' के दाहिने हाथ की ओर आगे नेस्टेड quantifications हो सकते हैं।
हाल ही में एमएलएफ के स्पष्ट रूप से टाइप किए गए संस्करण मौजूद नहीं थे। टाइप किए गए कंपाइलर ट्रांसफॉर्मेशन के लिए यह महत्वपूर्ण है (जैसे जीएचसी करता है)। Boris Yakobowski's PhD thesis का भाग 3 इस तरह के संस्करण पर पहला प्रयास है। (भाग 1 & 2 भी दिलचस्प हैं, वे "ग्राफिकल प्रकार" के माध्यम से MLF की एक अधिक सहज प्रतिनिधित्व का वर्णन।)
FPH करने के लिए वापस आ रहा है, इसके मूल विचार आंतरिक रूप से MLF तकनीक का उपयोग करने के लिए है, लेकिन प्रकार की आवश्यकता होती है let बाइंडिंग पर एनोटेशन। यदि आप केवल हिंडली/मिलनर प्रकार चाहते हैं, तो कोई टिप्पणी आवश्यक नहीं है। यदि आप उच्च-रैंक प्रकार चाहते हैं, तो आपको अनुरोधित प्रकार निर्दिष्ट करना होगा, लेकिन केवल let (या शीर्ष-स्तर) बाध्यकारी पर।
एफपीएच (एमएलएफ की तरह) अप्रासंगिक क्षणिकता का समर्थन करता है, इसलिए मुझे नहीं लगता कि आपकी समस्या लागू होती है। इसलिए इसे ऊपर f . g अभिव्यक्ति टाइप करने में कोई समस्या नहीं होनी चाहिए। हालांकि, एफएचएच अभी तक जीएचसी में लागू नहीं किया गया है और अधिकतर संभावना नहीं होगी। कठिनाइयों समानता दबाव (और संभवतः वर्ग की बाधाओं के प्रकार) के साथ बातचीत से आती हैं। मुझे यकीन नहीं है कि नवीनतम स्थिति क्या है, लेकिन मैंने सुना है कि एसपीजे अपर्याप्तता से दूर जाना चाहता है। वह सभी अभिव्यक्तिपूर्ण शक्ति लागत पर आती है, और अब तक कोई किफायती और समस्त समाधान नहीं मिला है।
आप कैसे प्रकार (रनस्ट हमेशा के लिए) काम कर सकते हैं? – Peaker