scala मूल्य, प्रकार, प्रकार,... एक अनंत अनुक्रम के रूप में?




haskell functional-programming (2)

शब्दावली type और kind अच्छी तरह से स्केल नहीं करता है। सिद्धांतकार टाइप करें क्योंकि बर्ट्रैंड रसेल ने "प्रकारों" का पदानुक्रम इस्तेमाल किया है। इसके एक संस्करण में Integer : Type 0, Type 0 : Type 1, Type 1 : Type 2, ..., Type n : Type (n+1), .... कोक और एग्डा जैसे निर्भर टाइप की गई भाषाओं में, एक को अक्सर इन "उच्च प्रकारों" की आवश्यकता होती है।

रसेल के विरोधाभास से बचने के लिए इस तरह के स्तर सहायक हैं। Type : Type का उपयोग Type : Type विरोधाभास का कारण बनता है (वैकल्पिक डिजाइन के लिए Quine देखें)।

संख्याओं का यह उपयोग मानक संकेत है जब हमें इसकी आवश्यकता होती है। कुछ प्रकार के सिद्धांतों में "संचयी प्रकार", "संचयी स्तर" या "संचयी प्रकार" की धारणा होती है जो कहती है "अगर t : Type n तो t : Type (n+1) "।

संचयी स्तर + "स्तर बहुरूपता" एक सिद्धांत को Type : Type रूप में लगभग लचीला देता है, लेकिन विरोधाभास से बचाता है। कोक ज्यादातर स्तरों को निहित करता है, हालांकि Prop और Prop टाइप Type , Type {1} : Type {2} । यही है, आप आमतौर पर संख्याओं को नहीं देखते हैं, और अधिकांश समय यह सिर्फ काम करता है।

आगादा में एक भाषा प्रज्ञा है जो स्तर बहुरूपता प्रदान करती है, और चीजों को बहुत लचीला बनाती है, लेकिन थोड़ा नौकरशाही हो सकती है (हालांकि एग्डा आमतौर पर अन्य क्षेत्रों में कोक की तुलना में कम "नौकरशाही" है)।

एक और अच्छा शब्द "ब्रह्मांड" है।

मैं केवल प्रकार की अवधारणा से परिचित होना शुरू कर रहा हूं, इसलिए यदि मैं अपने प्रश्नों को अच्छी तरह से तैयार नहीं कर रहा हूं तो मेरे साथ सहन करें ...

मानों के प्रकार हैं:

3 :: Int
[1,2,3] :: [Int]
('c',True) :: (Char,Bool)

प्रकार के प्रकार हैं:

the type 'Int' has kind *
the type '[Int]' also has kind *
   but the type constructor [] has kind * -> *
similarly, the type (Char,Bool) has kind  *
   but the type constructor (,) has kind * -> * -> *

दयालु क्या है?

क्या उनके पास प्रकार, या शैलियों, नस्लों, या किस्में हैं?

अमूर्तता का यह अनुक्रम कितना दूर जाता है? क्या हम रुकते हैं क्योंकि हम शब्दों से बाहर निकलते हैं, या हम रोकते हैं क्योंकि आगे जाने से कोई मूल्य नहीं है? या, शायद, क्योंकि हम जल्दी से मानव संज्ञान की सीमा तक पहुंचते हैं और केवल हमारे सिर को उच्च-शैली वाले प्रकारों के चारों ओर लपेट नहीं सकते हैं?

एक संबंधित प्रश्न: भाषाएं मूल्य बनाने के लिए हमें मूल्य-निर्माणकर्ता (एक विपक्षी ऑपरेटर की तरह) देती हैं। भाषाएं हमें प्रकार बनाने के लिए (,) या [] जैसे प्रकार-रचनाकार भी देती हैं। क्या ऐसी कोई भाषाएं हैं जो प्रकार बनाने के लिए दयालु रचनाकारों का पर्दाफाश करती हैं?

एक और एज केस जो मैं उत्सुक हूं: हमारे पास स्पष्ट रूप से एक प्रकार है जिसका कोई मूल्य नहीं है, जिसे the कहा जाता है, जिसे "नीचे का प्रकार" कहा जाता है। क्या कोई ऐसा प्रकार है जिसमें कोई प्रकार नहीं है: नीचे की तरह?


आपको शायद ओमेगा के बारे में टिम शेर्ड का पेपर पढ़ना चाहिए, जो हास्केल की एक बोली है जो कि प्रकार / प्रकार / प्रकार के अनंत टॉवर के साथ है, लेकिन पूरी तरह से निर्भर प्रकारों के बिना। यह बताता है कि आप इसे क्यों चाहते हैं, और उल्लेख करते हैं कि "सॉर्ट" के ऊपर के स्तर अभ्यास में हैं (कम से कम अब तक) सीधे उपयोग नहीं किया जाता है।





higher-kinded-types