क्या जीएडीटी जीएचसी में टाइप असमानताओं को साबित करने के लिए इस्तेमाल किया जा सकता है?

Question

तो, करने के लिए अपने चल रहे प्रयास में छोटे हास्केल व्यायाम के माध्यम से आधे को समझने करी-हावर्ड, मैं इस बिंदु पर अटक मिल गया है:

{-# LANGUAGE GADTs #-} 

import Data.Void 

type Not a = a -> Void 

-- | The type of type equality proofs, which can only be instantiated if a = b. 
data Equal a b where 
    Refl :: Equal a a 

-- | Derive a contradiction from a putative proof of @Equal Int Char@. 
intIsNotChar :: Not (Equal Int Char) 
intIsNotChar intIsChar = ??? 

जाहिर प्रकार Equal Int Char, कोई (गैर नीचे) निवासी हैं और इस प्रकार अर्थात् वहां absurdEquality :: Equal Int Char -> a फ़ंक्शन होना चाहिए ... लेकिन मेरे जीवन के लिए मैं undefined का उपयोग करने के अलावा किसी अन्य को लिखने का कोई तरीका नहीं समझ सकता।

तो या तो:

1. मैं कुछ याद कर रहा हूँ, या
2. भाषा है कि इस एक असंभव कार्य करता है में से कुछ सीमा है, और मैं समझता हूँ कि यह क्या है में कामयाब नहीं किया है।

मुझे संदेह है कि उत्तर ऐसा कुछ है: संकलक इस तथ्य का फायदा उठाने में असमर्थ है कि Equal ऐसे रचनाकार नहीं हैं जिनके पास = बी नहीं है। लेकिन अगर ऐसा है, तो यह क्या सच बनाता है?

Answer 1

यहां फिलिप जेएफ के समाधान का एक छोटा संस्करण है, जिस तरह से निर्भर प्रकार के सिद्धांतवादी वर्षों से समीकरणों को अस्वीकार कर रहे हैं।

type family Discriminate x 
type instance Discriminate Int =() 
type instance Discriminate Char = Void 

transport :: Equal a b -> Discriminate a -> Discriminate b 
transport Refl d = d 

refute :: Equal Int Char -> Void 
refute q = transport q() 

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

इस समस्या को हल करने के लिए undefined का उपयोग करना आवश्यक नहीं है। कभी-कभी कुल प्रोग्रामिंग में असंभव इनपुट को अस्वीकार करना शामिल है। यहां तक ​​कि undefined भी उपलब्ध है, मैं इसका उपयोग नहीं करने की अनुशंसा करता हूं जहां कुल विधि पर्याप्त है: कुल विधि बताती है क्यों कुछ असंभव है और टाइपशेकर पुष्टि करता है; undefined केवल दस्तावेज आपका वादा।दरअसल, अस्वीकार करने की यह विधि यह है कि एपिग्राम "असंभव मामलों" के साथ कैसे निपटता है जबकि यह सुनिश्चित करता है कि केस विश्लेषण अपने डोमेन को कवर करता है।

कम्प्यूटेशनल व्यवहार का सवाल है, ध्यान दें कि refute, के माध्यम से transportq में जरूरी सख्त है और वह q खाली संदर्भ में सामान्य रूप सिर, बस क्योंकि ऐसी कोई सिर सामान्य रूप से मौजूद है (गणना नहीं कर सकते हैं और क्योंकि गणना, प्रकार को बरकरार रखता है की पाठ्यक्रम)। कुल सेटिंग में, हम सुनिश्चित होंगे कि refute रन टाइम पर कभी भी नहीं बुलाया जाएगा। हास्केल में, हम कम से कम निश्चित हैं कि इससे पहले कि हम इसका जवाब देने के लिए बाध्य हैं, उसका तर्क अलग हो जाएगा या अपवाद फेंक देगा। एक आलसी संस्करण, जैसे

absurdEquality e = error "you have a type error likely to cause big problems" 

e की विषाक्तता ध्यान न दें और आपको बता यदि आप एक प्रकार की त्रुटि है कि जब आप नहीं करेंगे। मैं

absurdEquality e = e `seq` error "sue me if this happens" 

यदि ईमानदार अस्वीकार कड़ी मेहनत की तरह बहुत अधिक है।

Answer 2

मुझे undefined का उपयोग करने में समस्या को समझ में नहीं आता है हर प्रकार हास्केल में नीचे स्थित है। हमारी भाषा दृढ़ता से सामान्य नहीं है ... आप गलत चीज़ की तलाश में हैं। Equal Int Charटाइप त्रुटियों अच्छी तरह से अपवादों को अच्छी तरह से नहीं ले जाता है। देखें

{-# LANGUAGE GADTs, TypeFamilies #-} 

data Equal a b where 
    Refl :: Equal a a 

type family Pick cond a b 
type instance Pick Char a b = a 
type instance Pick Int a b = b 

newtype Picker cond a b = Picker (Pick cond a b) 

pick :: b -> Picker Int a b 
pick = Picker 

unpick :: Picker Char a b -> a 
unpick (Picker x) = x 

samePicker :: Equal t1 t2 -> Picker t1 a b -> Picker t2 a b 
samePicker Refl x = x 

absurdCoerce :: Equal Int Char -> a -> b 
absurdCoerce e x = unpick (samePicker e (pick x)) 

आप समारोह बनाने के लिए इस का उपयोग कर सकते आप

absurdEquality e = absurdCoerce e() 

चाहते हैं, लेकिन है कि इसकी गणना नियम के रूप में अपरिभाषित व्यवहार का उत्पादन करेगा। false प्रोग्राम को निरस्त करने के लिए, या कम से कम हमेशा के लिए चलाने के कारण होना चाहिए। निरस्त करना गणना गणना नियम है जो कम से कम तर्क को अंतर्दृष्टिवादी तर्क में जोड़ने के समान नहीं है। सही परिभाषा

absurdEquality e = error "you have a type error likely to cause big problems" 

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