क्या कोई कारण है कि हम डेटाकिंड्स के साथ प्रकारों को पॉप्युलेट नहीं कर सकते हैं?

Question

DataKinds के साथ, जैसे

data KFoo = TFoo 

एक परिभाषा तरह KFoo :: BOX और प्रकार TFoo :: KFoo परिचय देता है। क्यों नहीं मैं तो

data TFoo = CFoo 

ऐसी है कि CFoo :: TFoo, TFoo :: KFoo, KFoo :: BOX परिभाषित करने के लिए पर जा सकते हैं?

क्या सभी रचनाकारों को * से संबंधित किसी प्रकार से संबंधित होना चाहिए? यदि हां, तो क्यों?

संपादित: जब मैं यह कर मैं कोई त्रुटि मिलती नहीं है, क्योंकि निर्माणकर्ता और प्रकार एक नाम स्थान साझा करते हैं, लेकिन क्योंकि यह नियमित प्रकार के बजाय पदोन्नत कंस्ट्रक्टर्स के रूप में नाम स्पष्ट रूप से दिखाता GHC संघर्ष अनुमति देता है। प्रमोटेड कन्स्ट्रक्टर को संदर्भित करने के लिए दस्तावेज़ ' के साथ उपसर्ग करने के लिए कहते हैं। जब मैं

data 'TFoo = CFoo 

करने के लिए बदल कि दूसरी पंक्ति मैं त्रुटि प्रकार या वर्ग घोषणा के

विकृत सिर मिलती है: TFoo

Answer 1

सभी कंस्ट्रक्टर्स एक प्रकार के हैं की जरूरत है यह * के प्रकार से संबंधित है?

हां। यह वही है जो * का अर्थ है: यह है (उठाया/बॉक्स किया गया, मैं उस भाग के बारे में कभी भी निश्चित नहीं हूं) हास्केल प्रकार। वास्तव में अन्य सभी प्रकार वास्तव में प्रकार के प्रकार नहीं हैं हालांकि वे type वाक्यविन्यास साझा करते हैं। इसके बजाय * मेटाटाइप-स्तरीय प्रकार प्रकारों के लिए है, और अन्य सभी प्रकार मेटाटाइप-स्तरीय प्रकार हैं जो कि प्रकार नहीं हैं लेकिन रचनाकार या कुछ अलग टाइप करें।

(फिर से, वहाँ भी अनबॉक्स्ड प्रकार प्रकार के बारे में कुछ है,। उन निश्चित प्रकार के होते हैं, लेकिन मुझे लगता है कि यह एक data निर्माता के लिए संभव नहीं है)

Answer 2

सभी कंस्ट्रक्टर्स एक प्रकार के हैं की जरूरत है कि दयालु * से संबंधित है? यदि हां, तो क्यों? DataKinds संकलन के दौरान मिट हो:

सबसे महत्वपूर्ण कारण है कि वे प्रकार * (या #) का होना चाहिए चरण जुदाई GHC द्वारा नियोजित है। हम उन्हें केवल परोक्ष रूप से रनटाइम, सिंगलटन GADT डेटाटाइप्स को परिभाषित करते हुए प्रतिनिधित्व कर सकते हैं:

{-# LANGUAGE DataKinds #-} 

data Nat = Z | S Nat 

data SNat n where 
    SZ :: SNat Z 
    SS :: SNat n -> SNat (S n) 

लेकिन DataKind सूचकांक खुद को अभी भी क्रम मौजूद नहीं हैं। विभिन्न प्रकार चरण पृथक्करण के लिए एक सरल नियम प्रदान करते हैं, जो आश्रित प्रकारों के साथ सीधा नहीं होगा (भले ही यह संभावित रूप से प्रकार स्तर प्रोग्रामिंग को सरल बनाये)।