क्या निर्माण के कैलकुस से "पीआई" को हटाना वास्तव में संभव है?

Question

लेख Simpler, Easier! दावा करता है कि "पीआई" की उपस्थिति के बिना भी निर्भर प्रकार प्रणाली को एन्कोड करना संभव हो सकता है - यानी, आप इसके लिए "लैम" कन्स्ट्रक्टर का पुन: उपयोग कर सकते हैं। लेकिन यह कैसे सच हो सकता है, अगर कुछ मामलों में "पीआई" और "लैम" का अलग-अलग व्यवहार किया जाता है?

इसके अलावा, "स्टार" हटाया जा सकता है? मुझे लगता है कि आप "λ x। X" (id) द्वारा इसकी सभी घटनाओं को प्रतिस्थापित कर सकते हैं।

Answer 1

यह हैस्केल में (a, b) की तरह अधिभारित है: यह एक प्रकार और एक मूल्य दोनों हो सकता है। आप Π और λ के लिए एक ही बाइंडर का उपयोग कर सकते हैं और टाइपशेकर उस संदर्भ से निर्णय लेगा जिसका आप मतलब है। यदि आप किसी अन्य के खिलाफ एक बांधने की मशीन typecheck, तो पूर्व λ है और बाद Π है - और कि तुम क्यों नहीं स्पष्ट रूप λ x . x साथ * की जगह ले सकता है - क्योंकि तब पूर्व बांधने की मशीन Π हो सकता है और बाद * (* एक बंधक के रूप में है मुझे कोई समझ नहीं आता है)। ∀ = λ और * = λ x . x के साथ एक बड़ी समस्या है: * = ∀ x . x द्वारा False को पोस्ट करने का एक आम तरीका है - इस प्रकार को ध्वनि प्रणाली में निर्वासित होना चाहिए, इसलिए आपके पास कोई भी प्रकार नहीं होगा।

"forall और मज़ा के बीच समानता" Coq-क्लब पर हाल ही में धागा था (gmane.org मुझे "ऐसा कोई संदेश" देता है, यह सिर्फ मुझे है?), यहाँ कुछ अंश इस प्रकार हैं:

डोमिनिक मुलिगन:

http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf

:

और यहाँ एक छोटा सा ग्रंथ सूची इसी तरह के कार्य की ओर इशारा करते के साथ एक और है विडंबना यह है कि, उस पेपर के मुताबिक, कोक्वांड ने पहले ऑटोमाथ में डी ब्रुज़न द्वारा स्थापित पर एक सम्मेलन के बाद, एकल, एकीकृत बाइंडर के साथ का कैलकुलेशन प्रस्तुत किया था।

Thorsten Altenkirch:

एक समारोह और उसके प्रकार बहुत अलग अवधारणाओं, भले ही वे कुछ सतही वाक्यात्मक समानता है कर रहे हैं।

विशेष रूप से नवागंतुक के लिए यह पहचान बहुत भ्रमित है और पूरी तरह से भ्रामक है। मुझे लगता है कि किसी को सैद्धांतिक अवधारणाओं को समझना चाहिए कि वे क्या मतलब रखते हैं और नहीं कि वे कैसा दिखते हैं।

एंड्रियास हाबिल:

मेरे छात्र मथायस Benkard भी एक ऐसी प्रणाली पर काम किया, "प्रकार प्रकार बिना जांच रहा है"

http://www.cse.chalmers.se/~abela/benkardThesis.pdf

ध्यान दें कि पहले लिंक पर वर्णित प्रणाली में Π-कमी (यानीआप lambdas की तरह पीआई-प्रकारों को लागू कर सकते हैं) - यदि आपके पास Π और λ आंतरिक रूप से (वाक्य रचनात्मक रूप से विपरीत) को एकीकृत करते हैं, तो आपके सिस्टम में भी यह होगा। और प्रणाली दूसरी कड़ी में वर्णित प्रकार सम्मिलित है और महत्व देता

एक तत्काल परिणाम प्रकार और उनके निवासियों के बीच कोई भेद का अभाव है: हर मूल्य एक प्रकार ही और अपने हिस्से के सभी युक्त; और इसके विपरीत, हर प्रकार एक समग्र मूल्य है जिसमें इसके निवासियों शामिल हैं।

तो वहाँ वास्तव में सिर्फ एक बांधने की मशीन (let और शायद fix को छोड़कर) है।