प्रकार स्तरीय अलगाव

Question

मैं प्रकार स्तरीय अलगाव परिभाषित किया है इस प्रकार की idempotency साबित:

{-# LANGUAGE DataKinds, TypeFamilies #-} 

type family Or (a :: Bool) (b :: Bool) :: Bool 
type instance Or False a = a 
type instance Or True a = True 

अब मैं (हास्केल में) साबित होता है कि यह idempotent है चाहते हैं। जो है, मैं प्रकार

idemp :: a ~ b => proxy (Or a b) -> proxy a 

जो प्रचालन id के बराबर है के साथ एक अवधि idemp निर्माण करना चाहते हैं। (जाहिर है, मैं इसे परिभाषित कर सकता हूं जैसे unsafeCoerce, लेकिन यह धोखाधड़ी है।)

क्या यह संभव है?

Answer 1

जो चीज आप पूछते हैं वह संभव नहीं है, लेकिन इसके बजाय कुछ ऐसा हो सकता है। यह संभव नहीं है क्योंकि सबूत को टाइप लेवल बूलियन पर केस विश्लेषण की आवश्यकता होती है, लेकिन आपके पास कोई डेटा नहीं है जो आपको ऐसा ईवेंट करने में सक्षम बनाता है। फिक्स एक सिंगलटन के माध्यम से ऐसी जानकारी शामिल करना है।

सबसे पहले, मुझे ध्यान दें कि idemp के लिए आपका प्रकार थोड़ा अपरिवर्तित है। बाधा a ~ b बस एक ही चीज़ को दो बार नाम देती है। निम्नलिखित typechecks:

idemq :: p (Or b b) -> p b 
idemq = undefined 
idemp :: a ~ b => p (Or a b) -> p a 
idemp = idemq 

(आप की कोई समस्या a ~ t जहां ta शामिल नहीं करता है, तो यह a के लिए t विकल्प आमतौर पर अच्छा है अपवाद instance घोषणाओं में है:। एक उदाहरण के सिर कुछ भी से मेल खाएगी में एक a , इसलिए उदाहरण तब भी आग लग जाएगा जब तक कि यह बात अभी तक t बन गई है। लेकिन मैं digress।)

मेरा दावा है कि idemq अविश्वसनीय है क्योंकि हमारे पास b के बारे में कोई उपयोगी जानकारी नहीं है। उपलब्ध एकमात्र डेटा p में कुछ है, और हम नहीं जानते कि p क्या है।

हमें b पर मामलों के कारणों की आवश्यकता है। ध्यान रखें कि सामान्य रिकर्सिव प्रकार के परिवारों के साथ, हम टाइप लेवल बूलियन परिभाषित कर सकते हैं जो न तो True और न ही False हैं। अगर मैं UndecidableInstances पर स्विच, मैं परिभाषित कर सकते हैं

type family Loop (b :: Bool) :: Bool 
type instance Loop True = Loop False 
type instance Loop False = Loop True 

तो Loop TrueTrue या False, और स्थानीय स्तर पर भी बदतर करने के लिए कम नहीं किया जा सकता है, वहाँ कि

Or (Loop True) (Loop True) ~ Loop True  -- this ain't so 

वहाँ इसे से बाहर कोई रास्ता नहीं है दिखाने के लिए कोई रास्ता नहीं है । हमें रन टाइम सबूत चाहिए कि हमारे b अच्छी तरह से व्यवहार किए गए बूलियनों में से एक है जो किसी भी तरह के मूल्य पर गणना करता है। हमें इसलिए गाना

data Booly :: Bool -> * where 
    Truey :: Booly True 
    Falsey :: Booly False 

तो हम जानते हैं कि Booly b, हम एक मामले विश्लेषण जो हमें बताएगा कि क्या b का पता लगा सकते हैं। फिर प्रत्येक मामले अच्छी तरह से गुजर जाएगा। p b पर उपयोग करने के बजाय तथ्यों को पैक करने के लिए PolyKinds के साथ परिभाषित समानता प्रकार का उपयोग करके मैं इसे कैसे खेलूँगा।

data (:=:) a b where 
    Refl :: a :=: a 

हमारे महत्वपूर्ण तथ्य अब स्पष्ट रूप से कहा गया है और सिद्ध:

orIdem :: Booly b -> Or b b :=: b 
orIdem Truey = Refl 
orIdem Falsey = Refl 

और हम सख्त मामले विश्लेषण से इस तथ्य को तैनात कर सकते हैं: करने के लिए,

idemp :: Booly b -> p (Or b b) -> p b 
idemp b p = case orIdem b of Refl -> p 

मामले विश्लेषण सख्त होना चाहिए जांचें कि सबूत कुछ लूपी झूठ नहीं है, बल्कि भलाई के लिए ईमानदार Refl चुपचाप Or b b ~ b के सबूत को पैक कर रहा है जिसे टाइप को ठीक करने की आवश्यकता है तों।

यदि आप स्पष्ट रूप से इन सभी सिंगलटन मानों को स्लिंग करना नहीं चाहते हैं, तो आप कोसमिक सुझाव देते हैं, उन्हें एक शब्दकोश में छुपाएं और उन्हें केवल तभी निकालें जब आपको उनकी आवश्यकता हो।

रिचर्ड ईसेनबर्ग और स्टीफनी वीरिच में एक टेम्पलेट हास्केल लाइब्रेरी है जो आपके लिए इन परिवारों और कक्षाओं को मिटती है। वह उन्हें भी निर्माण और आप

orIdem pi b :: Bool. Or b b :=: b 
orIdem {True} = Refl 
orIdem {False} = Refl 

बारे में जहां pi b :: Bool.forall b :: Bool. Booly b -> के लिए विस्तारित की सुविधा देता है सकते हैं।

लेकिन यह इतना ही पालावर है। यही कारण है कि मेरा गिरोह एक गैर-पैरामीट्रिक क्वांटिफ़ायर (forall और -> से अलग) होने के कारण हस्केल को वास्तविक pi जोड़ने पर काम कर रहा है, जिसे हास्केल के प्रकार और अवधि भाषाओं के बीच अब नॉनट्रिविअल चौराहे में सामान द्वारा तत्काल किया जा सकता है। यह pi में "अंतर्निहित" संस्करण भी हो सकता है, जहां तर्क डिफ़ॉल्ट रूप से छुपा रहता है। दोनों क्रमशः सिंगलटन परिवारों और कक्षाओं का उपयोग करने के अनुरूप हैं, लेकिन अतिरिक्त किट प्राप्त करने के लिए डेटाटाइप को तीन बार परिभाषित करने की आवश्यकता नहीं है।

यह उल्लेखनीय हो सकता है कि कुल प्रकार के सिद्धांत में, यह है जो रन समय पर बूलियन b की अतिरिक्त प्रति को पारित करने के लिए आवश्यक है। बात यह है कि, b का उपयोग केवल यह प्रमाण बनाने के लिए किया जाता है कि डेटा p (Or b b) से p b तक ले जाया जा सकता है, डेटा को परिवहन के लिए जरूरी नहीं है। हम रन टाइम पर बाइंडर्स के तहत गणना नहीं करते हैं, इसलिए समीकरण के बेईमान प्रमाण को पकाए जाने का कोई तरीका नहीं है, इसलिए हम सबूत घटक और b की प्रतिलिपि मिटा सकते हैं जो इसे वितरित करता है। जैसा कि रैंडी पोलैक कहते हैं, दृढ़ता से सामान्यीकृत कैलकुस में काम करने के बारे में सबसे अच्छी बात यह है कि चीजों को सामान्यीकृत नहीं करना है।

Answer 2

जैसा कि जॉन एल ने अपनी टिप्पणी में कहा है, वर्तमान में अतिरिक्त बाधाओं के बिना ऐसा करने का कोई तरीका नहीं है, जहां तक ​​मुझे पता है। आप इस तथ्य का फायदा नहीं उठा सकते कि Bool शब्द स्तर पर एक बंद प्रकार है, और idemp में Bool के प्रकार चर पर केस विश्लेषण करने का कोई तरीका नहीं है।

ठेठ समाधान सिंगलटन प्रकार का उपयोग अवधि स्तर पर Bool तरह संरचना को प्रतिबिंबित करने के लिए है:

data SBool :: Bool -> * where 
    SFalse :: SBool False 
    STrue :: SBool True 

किसी भी b :: Bool के लिए, वहाँ (बेशक सापेक्ष undefined,) SBool b का सिर्फ एक निवासी है।

SBool के साथ, प्रमेय साबित करने के लिए आसान है (, मैं नहीं जानता कि क्यों आप अतिरिक्त समानता बाधा जोड़ा मैं इसे दूर करने के लिए जा रहा हूँ):

idemp' :: SBool a -> proxy (Or a a) -> proxy a 
idemp' SFalse x = x 
idemp' STrue x = x 

इसके बजाय तर्क स्पष्टतः पास की, आप इसे परोक्ष पारित कर सकते हैं, एक वर्ग है कि SBool प्रतिनिधित्व बना सकते हैं परिभाषित करते हुए:

class CBool (b :: Bool) where 
    sBool :: SBool b 

instance CBool True where sBool = STrue 
instance CBool False where sBool = SFalse 

तब:

idemp :: CBool a => proxy (Or a a) -> proxy a 
idemp = idemp' sBool 

मुझे नहीं लगता कि आप CBool बाधा से छुटकारा पा सकते हैं, लेकिन यह किसी भी a :: Bool के लिए बहुत ही सही है, इसलिए यह एक बहुत ही मजबूत धारणा नहीं है।