इडिस में, क्या मैं मुक्त प्रमेय साबित कर सकता हूं, उदा। टाइप 'फॉरल टी' का एकमात्र (कुल) फ़ंक्शन। टी -> टी` `आईडी` है?

Question

पर्याप्त पॉलिमॉर्फिक प्रकारों के लिए, पैरामीट्रिकिटी विशिष्ट रूप से फ़ंक्शन को निर्धारित कर सकती है (विवरण के लिए Wadler's Theorems for free! देखें)। उदाहरण के लिए, टाइप forall t. t -> t के साथ एकमात्र कुल फ़ंक्शन पहचान फ़ंक्शन id है।

क्या यह इडिस में यह साबित करना और साबित करना संभव है? (और यदि यह इडिस के अंदर साबित नहीं किया जा सकता है, तो क्या यह सच है?)

मेरा प्रयास है (मुझे पता है कि कार्य समानता इडिस में एक प्राचीन अवधारणा नहीं है, इसलिए मैं सामान्य प्रकार के किसी भी कार्य का दावा करता हूं t -> t हमेशा एक ही परिणाम देता है के रूप में पहचान समारोह वापसी होगी):

%default total 

GenericEndomorphism: Type 
GenericEndomorphism = (t: Type) -> (t -> t) 

id_is_an_example : GenericEndomorphism 
id_is_an_example t = id 

id_is_the_only_example : (f : GenericEndomorphism) -> (t : Type) -> (x : t) -> f t x = x 
id_is_the_only_example f t x = ?id_is_the_only_example_rhs 

जिसके परिणामस्वरूप छेद है:

- + Main.id_is_the_only_example_rhs [P] 
`--        f : GenericEndomorphism 
            t : Type 
            x : t 
    ------------------------------------------------------- 
     Main.id_is_the_only_example_rhs : f t x = x 

Answer 1

आप नहीं कर सकते। इस तरह के प्रमेय ("मुक्त प्रमेय") इस धारणा से पालन करते हैं कि प्रकार सार हैं और आप पैटर्न पर मिलान नहीं कर सकते हैं या किसी भी तरह से अपनी संरचना को समझ सकते हैं। लेकिन आप इडिस में आंतरिक रूप से प्रकारों के लिए अमूर्तता की संपत्ति को व्यक्त नहीं कर सकते हैं। टाइप सिद्धांत के मुख्यधारा के कार्यान्वयन से यह संभव नहीं है। Type theory in color में यह सुविधा है लेकिन यह बहुत जटिल है और इसका कोई व्यावहारिक कार्यान्वयन नहीं है।

आप अभी भी मुफ्त प्रमेय को पोस्ट कर सकते हैं और उनका उपयोग कर सकते हैं, लेकिन आपको यह सुनिश्चित करना होगा कि वे उन चीज़ों के मूल्यांकन को अवरुद्ध न करें जिन्हें आप मूल्यांकन करना चाहते हैं।