आप कैसे साबित करते हैं कि एक फ़ंक्शन इसके प्रकार के लिए अद्वितीय है?

Question

id टाइप a -> a, और fst का एकमात्र कार्य प्रकार (a,b) -> a का एकमात्र कार्य है। इन साधारण मामलों में, यह देखने के लिए काफी सरल है। लेकिन सामान्य रूप से, आप इसे साबित करने के बारे में कैसे जाएंगे? क्या होगा यदि एक ही प्रकार के कई संभावित कार्य हैं?

वैकल्पिक रूप से, फ़ंक्शन के प्रकार को देखते हुए, आप उस प्रकार के अद्वितीय (यदि यह सत्य है) फ़ंक्शन कैसे प्राप्त करते हैं?

संपादित करें: मुझे विशेष रूप से रुचि है जब हम प्रकारों में बाधाओं को जोड़ना शुरू करते हैं।

Answer 1

परिणाम जो आप रेनॉल्ड्स की पैरामीट्रिकिटी से प्राप्त कर रहे हैं, और सबसे प्रसिद्ध रूप से वेडलर द्वारा theorems for free में दिखाया गया था।

मैंने मूलभूत पैरामीट्रिकिटी परिणामों को साबित करने का सबसे शानदार तरीका देखा है जिसे मैंने "सिंगलटन टाइप" की धारणा का उपयोग किया है। अनिवार्य रूप से, किसी भी एडीटी

दिया

data Nat = Zero | Succ Nat 

एक अनुक्रमित परिवार (यह भी एक GADT के रूप में जाना)

data SNat n where 
    SZero :: SNat Zero 
    SSucc :: SNat n -> SNat (Succ n) 

वहाँ मौजूद है और हम से एक untyped करने के लिए "मिटा" सभी प्रकार हमारी भाषा के लिए एक अर्थ विज्ञान दे सकते हैं भाषा जैसे Nat और SNat एक ही चीज़ को मिटा दें। फिर, उस भाषा

id (x :: SNat n) :: SNat n 

SNat n है केवल एक निवासी (अपने सिंगलटन), अर्थ विज्ञान के बाद से विलोपन द्वारा दिया जाता है की टाइपिंग नियमों से, कार्यों उनके तर्क का प्रकार, इसलिए केवल मूल्य से वापस उपयोग नहीं कर सकते किसी भी Nat पर id वह नंबर है जिसे आपने दिया था। अधिकांश मूलभूत परिणामों को साबित करने के लिए इस मूल तर्क को बढ़ाया जा सकता है और A Simple Proof Technique for Parametricity Results में कार्ल क्रैरी द्वारा उपयोग किया गया था, हालांकि मेरे पास प्रेजेंटेशन Stone and Harper