0 के सभी उदाहरणों का सामान्य सुपरटेप क्या है, मैं ऑटोलॉजी डिज़ाइन करने की कोशिश कर रहा हूं जैसे कि ओडब्लूएल या टॉपिक मैप्स के साथ परिभाषित किया जा सकता है जिसमें पॉलिमॉर्फिक प्रकारों जैसे सूची [टी] के लिए समर्थन शामिल है, जहां टी एक है अंतराल प्रकार (कुछ भी नहीं, कोई भी) का पैरामीटर टाइप करें और सूची फंक्शन प्रकार * -> * है। आखिरकार, मैं अर्थपूर्ण भाषा में एक प्रकार की प्रणाली ऑटोलॉजी का वर्णन पर्याप्त विस्तार और कठोरता के साथ करना चाहता हूं कि यह समान अर्थपूर्ण भाषा में लिखे गए टाइप-सेफ सॉफ़्टवेयर कोड का आधार हो सकता है।टाइप इन थ्योरी
इस लक्ष्य को ध्यान में रखते हुए, मैं प्रकारों की एक श्रेणीबद्ध संरचना को समझने की कोशिश कर रहा हूं जहां प्रकार, अंतराल प्रकार और कार्य प्रकार सभी प्रकार के उदाहरण हैं। क्या सभी प्रकार के आम 'सुपरकिंड' के लिए औपचारिक नाम है? सबसे अच्छा शब्द मैं 'दयालु उदाहरण' के साथ आ सकता हूं। क्या यह टाइप सिद्धांत में भी एक सार्थक अवधारणा है? यहां तक कि यदि ऐसा नहीं है, तो मुझे ऐसी अवधारणा की आवश्यकता है जैसे कि (टॉपिक मैप्स टर्मिनोलॉजी में) "फ़ंक्शन-तर्क-प्रकार-बाधा संघ में एक भूमिका 'अनुमत-प्रकार' है जिसका खिलाड़ी प्रकार का होना चाहिए 'Kind Instance ' "।
इसके अलावा, मैंने केवल इस परियोजना के लिए खुद को सिद्धांत लिखने शुरू कर दिया है और मुझे इसे पूरा करने में सक्षम होने से पहले सीखने के लिए बहुत कुछ है। मैंने टाइप-थ्योरी पर कुछ स्केल-संबंधित पेपर पढ़े हैं जिनमें जेनिक्स ऑफ हायर किंड (http://adriaanm.github.com/files/higher.pdf) शामिल हैं और स्कैला में सुरक्षित टाइप-स्तरीय एब्स्ट्रक्शन के माध्यम से अपना रास्ता काम करना शुरू कर दिया है (http://adriaanm.github.com/files/scalina-final.pdf) और Type Constructor Polymorphism for Scala[pdf]। मुझे स्कैला की तुलना में हास्केल से कम परिचितता है लेकिन मुझे कुछ प्रासंगिक दिखने वाले कागजात जैसे System F with Type Equality Coercions[pdf] का सामना करना पड़ा है कि मुझे समझने के लिए हास्केल की एक और अधिक उन्नत समझ की आवश्यकता होगी। यदि कोई शुरुआती स्तर से शुरू होने वाले हास्केल के प्रकार की प्रणाली सीखने और सामान्यीकृत बीजगणितीय डेटा प्रकार जैसे उन्नत सिद्धांतों के लिए अग्रणी तरीके से सीखने के लिए पढ़ने की सामग्री की प्रगति का सुझाव दे सकता है, तो इसकी भी सराहना की जाएगी।
अंत में, यदि आप ओडब्लूएल या टॉपिक मैप्स जैसे अर्थात् ऑटोलॉजी भाषा में किसी प्रकार की प्रणाली का वर्णन करने के मौजूदा प्रयासों के बारे में जानते हैं, या यदि आपके पास ऐसा करने के बारे में कोई सुझाव है, तो मुझे यह भी सुनना अच्छा लगेगा।
आईआईयूसी, निर्भर प्रकारों और 'टाइप: टाइप' नियम के साथ, ऐसे प्रोग्राम मौजूद हैं जो एक प्रकार की जांचकर्ता को अनंत लूप का कारण बनेंगे - लेकिन उन कार्यक्रमों को दूर करना बहुत कठिन प्रयास करना है, यह नहीं है एक रोजमर्रा की घटना - इसलिए यदि आपके पास सबूतों के बजाय कार्यक्रम हैं, तो इसके निरंतर विकल्पों की तुलना में 'टाइप: टाइप' की सादगी शायद बलिदान के लायक है। – luqui
क्या आप मुझे "टाइप: टाइप" नियम समझाते हुए कुछ लिंक दे सकते हैं और अभ्यास का उपयोग कहां किया जा सकता है इसका एक उदाहरण दें। साथ ही, क्या प्रोग्राम को रोकने या पहचानने का कोई तरीका है जो अनंत लूप का कारण बनता है? यह मेरे द्वारा ध्यान में रखे गए एप्लिकेशन में एक सुरक्षा समस्या बन सकता है क्योंकि इसमें तीसरे पक्ष द्वारा लिखे गए कोड को निष्पादित करना शामिल होगा। –
@ChrisBarnett CoqArt में 'टाइप: टाइप'' की कुछ चर्चा है; Google http://webcache.googleusercontent.com/search?q=cache:http://adam.chlipala.net/cpdt/html/Universes.html भी सुझाता है। अनंत लूप के लिए, ठीक है, मुझे यकीन है कि आप रोक समस्या के बारे में जानते हैं। असल में आपकी एकमात्र उम्मीद अगर आपको समाप्ति की जांच करने की आवश्यकता है तो कुछ रूढ़िवादी लिखना है, और फिर आप अनिवार्य रूप से कुछ रोचक कार्यक्रमों को रद्द कर देते हैं। कोक और आगादा में बहुत परिष्कृत समाप्ति चेकर्स हैं, लेकिन यहां तक कि प्रत्येक विकास के कुछ हिस्सों में टाइपशेकर की संतुष्टि को साबित करना शामिल है जो चीजें समाप्त होती हैं। –