मैं कुछ मौजूदा भाषा में किए गए नवीनतम व्यावहारिक परिवर्तन के बारे में सीखने के बजाय प्रकार के पीछे वास्तविक सिद्धांत को समझना चाहता हूं (उदाहरण के लिए, हास्केल या स्कैला की प्रकार प्रणाली कैसे काम करती है)।टाइप सिस्टम और टाइप थ्योरी का गहन अध्ययन
इस पृष्ठभूमि को लेने का सबसे अच्छा तरीका क्या है?
टाइप सिद्धांत एक बड़ा क्षेत्र है। सबसे पहले, शब्द "प्रकार" कुछ कारणों से कंप्यूटर विज्ञान में एक गलत नामक है, भले ही वे अधिकतर मूलभूत विचार के लिए उपयोग किए जाते हैं। ज्यादातर संदर्भों के लिए कई संदर्भ, दर्शन, कंप्यूटर विज्ञान और गणित में प्रकार उत्पन्न हुए हैं। गणित में प्रकारों की उत्पत्ति सेट सिद्धांत को औपचारिक बनाने और नट विरोधाभासों में चलने की कोशिश करने से आती है, हालांकि कंप्यूटर विज्ञान में समान विरोधाभास उत्पन्न होते हैं। (उदाहरण के लिए, मैं इस पर गिरार्ड के विरोधाभास को इंगित करना चाहता हूं)।
जिस तरह से आप संभवतः वर्तमान क्षण में प्रकारों की व्याख्या करते हैं वह एक विचार है जो कंप्यूटरों में 70 के दशक-9 0 के दशक में लोकप्रिय हो गया है: प्रकार हल्के प्रवाह असंवेदनशील विश्लेषण हैं जो हमें लिखने वाले कार्यक्रमों के बारे में संक्षिप्त तार्किक गारंटी देने की अनुमति देते हैं। इसके लिए प्रकार का उपयोग किया जा सकता है, लेकिन आप वास्तव में उन्हें उच्च ऑर्डर तर्क को एन्कोड करने के लिए सभी तरह से ले जा सकते हैं, जहां प्रोग्रामसबूत हैं। एक बार जब आप यहां जाते हैं, तो आप सबूत ले सकते हैं, कम्प्यूटेशनल घटक निकाल सकते हैं, और इसे एक ऐसे प्रोग्राम में बदल सकते हैं जो "सही" परिणाम (आपके द्वारा साबित प्रमेय के संबंध में) की गणना करता है।
में कुछ सड़कों तुम यहाँ से ले जा सकते हैं कर रहे हैं:
तुम भी कुछ संबंधित क्षेत्रों में देखना चाहते हो सकता है:
में कुछ बेहतरीन अनुशंसाओं मैं इससे भी आगे सीखने के लिए कर रहे हैं, लेकिन मैं निश्चित रूप से बेन पियर्स की किताबों के साथ शुरू होता है (मैं वास्तव में पुस्तक का पालन "प्रकार और कंप्यूटर विज्ञान में उन्नत विषयों में कभी नहीं मिल गया है, "लेकिन यह भी आपके लिए दिलचस्प है)। विशेष रूप से, मुझे उच्च क्रम प्रकार सिद्धांत पर एक महान लेख रखने वाले स्वचालित तर्क की हैंडबुक याद है।
पीएस, मुझे विश्वास है कि इस सवाल का जवाब वस्तुतः है हूँ, "एक पीएचडी। प्रोग्रामिंग भाषाओं में, दर्शन, या तर्क मिलता है ..." है कि इस सवाल का जवाब पाने के बाद ;-)
≈½ सप्ताह, मैं सिर्फ बेंजामिन की किताब पढ़ रहा हूं, और मुझे कहना है कि यह बहुत अच्छा नहीं है। सबसे पहले, पुस्तक को समझने के लिए गणित नोटेशन के साथ परिपक्वता की आवश्यकता होती है * (यह विचार कि विशेष पेपर या पुस्तक के लेखक द्वारा परिभाषित किए गए किसी भी को छोड़कर कोई नोटेशन नहीं है) *। दूसरे में, मैं सिर्फ λ-calculच्छी अध्याय के माध्यम से जा रहा हूं, और लेखक या तो अपने स्वयं के नोटेशन के स्पष्टीकरण में बुरा है, या कुछ सूत्र गलत हैं। और बीटीडब्ल्यू, * मुझे पता है λ-counti *! –
मैं सम्मान से असहमत हूं। मैंने टाइप सिद्धांत के अधिक सुलभ प्रारंभिक उपचार को नहीं देखा है। सभी नोटेशन को आर्थिक रूप से परिभाषित करने का विचार और फिर पारंपरिक बूटेशन (उधार, कहने, मॉडल सिद्धांत) के संदर्भ में, "बूटस्ट्रैप" शैली में शेष प्रकारों को परिभाषित करने के लिए इसका उपयोग पीएल में एक * कोर * विचार है । क्या आप सूत्रों को इंगित कर सकते हैं जो गलत हैं? मैंने पहले किताब के साथ पढ़ाया है और मुझे यकीन है कि लेखक जानना चाहेंगे। –
आह, ठीक है, मुझे लगता है कि मैं * (पृष्ठ 55 के निचले हिस्से में एक) * के लिए शिकायत करने जा रहा था, लेकिन एफडब्ल्यूआईडब्ल्यू मुझे लगता है कि इसमें लगभग 15-20 मिनट लग गए थे, जबकि मैं सोच रहा था/लिख रहा था कि वास्तव में क्या लगता है उस के साथ गलत हो। आम तौर पर पुस्तक मुझे एक भावना महसूस करती है कि लेखक अभी तक कुछ महत्वपूर्ण नहीं कह रहा है, इसलिए मैं ध्यान से ध्यान से सीखता हूं, लेकिन ऐसा कभी नहीं होता है। लेकिन शायद, टाइप थ्योरी यही है। अब, मेरे लिए यह सीधे हास्केल का अभ्यास करने और श्रेणी सिद्धांत * सीखने के लिए और अधिक उपयोगी लगता है (जो मुझे थोड़ा एटीएम पता है, और लगता है कि यह उपयोगी है) *। –