क्या ऐसे हस्ताक्षर हैं जो हास्केल सत्यापित नहीं कर सकते हैं?

Question

This paper सिस्टम एफ में उस प्रकार की अनुमान (जिसे पेपर में "टाइपिबिलिटी" कहा जाता है) स्थापित करता है, यह अनिश्चित है। जो मैंने कभी और कभी नहीं सुना है वह पेपर का दूसरा परिणाम है, अर्थात् एफ में "टाइप चेकिंग" भी अपरिहार्य है। यहां "टाइप चेकिंग" प्रश्न का अर्थ है: t शब्द, T टाइप करें और टाइपिंग पर्यावरण A, निर्णय A ⊢ t : T व्युत्पन्न है? यह सवाल अनावश्यक है (और यह कि यह टाइप करने योग्यता के सवाल के बराबर है) मेरे लिए आश्चर्यजनक है, क्योंकि ऐसा लगता है कि यह सहजता से लगता है कि यह जवाब देने के लिए एक आसान सवाल होना चाहिए।

लेकिन किसी भी मामले में, कि हास्केल दिया प्रणाली एफ (या F-ओमेगा, यहां तक ​​कि) पर आधारित है, प्रकार की जाँच के बारे में परिणाम सुझाने एक हास्केल अवधि t है कि वहाँ और प्रकार T ऐसी संकलक होगा कि करने के लिए प्रतीत होता है यह तय करने में असमर्थ रहें कि t :: T मान्य है या नहीं। यदि ऐसा है, तो मुझे उत्सुकता है कि इस तरह का एक शब्द और प्रकार क्या है ... यदि यह मामला नहीं है, तो मैं गलतफहमी क्या कर रहा हूं?

मुमकिन कागज एक रचनात्मक जवाब देने के लिए नेतृत्व करेंगे समझने, लेकिन मैं अपने गहराई से बाहर एक छोटे से कर रहा हूँ :)

Answer 1

यहाँ स्काला में स्की पथरी का एक प्रकार के स्तर का कार्यान्वयन के लिए एक उदाहरण है: http://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/

अंतिम उदाहरण एक असंबद्ध पुनरावृत्ति दिखाता है। यदि आप हास्केल में ऐसा करते हैं (और मुझे यकीन है कि आप कर सकते हैं), तो आपके पास "अवांछित अभिव्यक्ति" के लिए एक उदाहरण है।

Answer 2

टाइपिंग जांच को सिंटैक्स को उचित रूप से समृद्ध करके निर्णायक बनाया जा सकता है। उदाहरण के लिए, पेपर में, हमारे पास lambdas \x -> e के रूप में लिखा गया है; इसे टाइप करने के लिए, आपको अनुमानx का प्रकार होना चाहिए। हालांकि, एक उपयुक्त समृद्ध वाक्यविन्यास के साथ, इसे \x :: t -> e के रूप में लिखा जा सकता है, जो प्रक्रिया से अनुमान लगाने का काम लेता है। इसी प्रकार, पेपर में, वे टाइप-लेवल लैम्बडा को अंतर्निहित होने की अनुमति देते हैं; यानी, यदि e :: t, तो e :: forall a. t भी है। टाइपशेकिंग करने के लिए, आपको अनुमान लगाना होगा कि कब और कितने forall जोड़ना है, और उन्हें कब खत्म करना है। पहले के रूप में, आप वाक्य रचना जोड़कर इस अधिक नियतात्मक कर सकते हैं: हम दो नए अभिव्यक्ति रूपों /\a. e और e [t] और दो नए टाइपिंग नियम है कि कहते हैं अगर e :: t, तो /\a. e :: forall a. t, और अगर e :: forall a. t, तो e [t'] :: t [t'/a] (जहां t [t'/a] में कोष्ठक प्रतिस्थापन कोष्ठक हैं जोड़ने)। फिर सिंटैक्स हमें बताता है कि कब और कितने टोल जोड़ना है, और उन्हें कब खत्म करना है।

तो सवाल यह है कि: क्या हम हास्केल से पर्याप्त रूप से एनोटेटेड सिस्टम एफ शर्तों में जा सकते हैं? और जवाब हां है, हास्केल प्रकार प्रणाली द्वारा रखे गए कुछ महत्वपूर्ण प्रतिबंधों के लिए धन्यवाद। सबसे महत्वपूर्ण यह है कि सभी प्रकार रैंक एक * हैं। बहुत अधिक विस्तार के बिना, "रैंक" खोजने के लिए आपको -> कन्स्ट्रक्टर के बाईं ओर कितनी बार जाना है।

Int -> Bool -- rank 0? 
forall a. (a -> a) -- rank 1 
(forall a. a -> a) -> (forall a. a -> a) -- rank 2 

विशेष रूप से, यह पॉलीमोर्फिज्म को थोड़ा सा प्रतिबंधित करता है। हम रैंक एक प्रकार के साथ कुछ इस तरह टाइप नहीं कर सकते हैं:

foo :: (forall a. a -> a) -> (String, Bool) -- a rank-2 type 
foo polymorphicId = (polymorphicId "hey", polymorphicId True) 

अगले सबसे महत्वपूर्ण प्रतिबंध यह है कि प्रकार चर केवल monomorphic प्रकार द्वारा प्रतिस्थापित किया जा सकता है। (इसमें a जैसे अन्य प्रकार के चर शामिल हैं, लेकिनजैसे पॉलिमॉर्फिक प्रकार नहीं हैं।) यह इस बात को सुनिश्चित करता है कि प्रतिस्थापन रैंक-वन-नेस को संरक्षित करता है।

यह पता चला है कि यदि आप इन दो प्रतिबंधों को बनाते हैं, तो न केवल टाइप-इनफरेंस डिकिडेबल है, बल्कि आपको न्यूनतम प्रकार भी मिलते हैं।

यदि हम हास्केल से जीएचसी तक जाते हैं, तो हम न केवल टाइप करने योग्य के बारे में बात कर सकते हैं, लेकिन अनुमान कैसे एल्गोरिदम दिखता है। विशेष रूप से, जीएचसी में, ऐसे एक्सटेंशन होते हैं जो उपर्युक्त दो प्रतिबंधों को आराम देते हैं; उस सेटिंग में जीएचसी कैसे अनुमान लगाता है? खैर, जवाब यह है कि यह बस कोशिश भी नहीं करता है। यदि आप उन सुविधाओं का उपयोग करके शब्दों को लिखना चाहते हैं, तो आपको टाइपिंग एनोटेशन जोड़ना होगा जो हमने पैराग्राफ में वापस सभी तरह से बात की थी: आपको स्पष्ट रूप से एनोटेट करना होगा कि forall एस कैसे पेश किया जाए और हटा दिया जाए। तो, क्या हम एक शब्द लिख सकते हैं कि जीएचसी के टाइप-चेकर अस्वीकार करते हैं? हां, यह आसान है: बस गैर-एनोटेटेड रैंक-दो (या उच्चतर) प्रकार या अपर्याप्तता का उपयोग करें। उदाहरण के लिए, निम्नलिखित टाइप की जांच नहीं करता है, भले ही यह एक स्पष्ट प्रकार एनोटेशन है और रैंक-दो प्रकार के साथ typable है:

{-# LANGUAGE Rank2Types #-} 
foo :: (String, Bool) 
foo = (\f -> (f "hey", f True)) id 

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