स्कॉल्स क्या हैं?

Question

ईक! जीएचसीआई ने मेरे कोड में Skolems पाया!

... 
Couldn't match type `k0' with `b' 
    because type variable `b' would escape its scope 
This (rigid, skolem) type variable is bound by 
    the type signature for 
    groupBy :: Ord b => (a -> b) -> Set a -> Set (b, [a]) 
The following variables have types that mention k0 
... 

वे क्या हैं? वे मेरे कार्यक्रम के साथ क्या चाहते हैं? और वे भागने की कोशिश क्यों कर रहे हैं (असभ्य छोटे blighters)?

Answer 1

प्रारंभ करने के लिए, एक संदर्भ में एक "कठोर" प्रकार चर का अर्थ उस संदर्भ के बाहर एक क्वांटिफायर द्वारा बाध्य एक प्रकार चर है, जो इस प्रकार अन्य प्रकार चर के साथ एकीकृत नहीं किया जा सकता है।

यह एक लैम्ब्डा द्वारा बाध्य चर जैसे काम करता है: "बाहर" से लैम्बडा (\x -> ...) को देखते हुए, आप इसे जो भी मूल्य पसंद करते हैं, उसे लागू कर सकते हैं; लेकिन अंदर पर, आप बस यह तय नहीं कर सकते कि x का मान कुछ विशेष मूल्य होना चाहिए। लैम्ब्डा के अंदर x के लिए एक मूल्य चुनना बहुत मूर्खतापूर्ण लगता है, लेकिन यह "ब्लै ब्लाह, कठोर प्रकार चर, ब्ला ब्लाह" से मेल नहीं खा सकता है।

ध्यान दें कि, स्पष्ट forall क्वांटिफ़ायर का उपयोग किए बिना, किसी भी शीर्ष-स्तरीय प्रकार हस्ताक्षर में प्रत्येक प्रकार के चर के लिए forall निहित है।

बेशक, यह आपको वह त्रुटि नहीं है जो आपको मिल रही है। क्या "एस्केड टाइप वैरिएबल" का अर्थ भी सिल्लियर है - यह लैम्ब्डा (\x -> ...) होने और के बाहर लैम्बडा के स्वतंत्र मानों का उपयोग करने की कोशिश कर रहा है, स्वतंत्र रूप से इसे तर्क देने के लिए। नहीं, लैम्बडा को किसी चीज़ पर लागू नहीं करना और परिणाम मूल्य का उपयोग करना - मेरा मतलब है कि वास्तव में वैरिएबल स्वयं का उपयोग करके उस क्षेत्र के बाहर है जहां इसे परिभाषित किया गया है।

कारणों के साथ ऐसा हो सकता है (लैम्ब्डा के साथ उदाहरण के रूप में स्पष्ट रूप से बेतुका प्रतीत होता है) क्योंकि वहां "प्रकार चर" के दो विचार हैं: एकीकरण के दौरान, आपके पास "चर" अनिश्चित प्रकार का प्रतिनिधित्व करते हैं, जिसे फिर टाइप अनुमान के माध्यम से अन्य ऐसे चर के साथ पहचाना जाता है। दूसरी तरफ, आपके ऊपर वर्णित मात्राबद्ध प्रकार चर हैं जिन्हें विशेष रूप से संभावित प्रकारों के रूप में पहचाना जाता है।

लैम्ब्डा अभिव्यक्ति (\x -> x) के प्रकार पर विचार करें। पूरी तरह से अनिश्चित प्रकार a से शुरू करते हुए, हम देखते हैं कि यह एक तर्क लेता है और a -> b तक संकीर्ण करता है, फिर हम देखते हैं कि इसे इसके तर्क के समान कुछ प्रकार वापस करना होगा, इसलिए हम इसे a -> a पर संकीर्ण करते हैं। लेकिन अब यह किसी भी प्रकार a के लिए काम करता है जो आप चाहते हैं, इसलिए हम इसे क्वांटिफायर (forall a. a -> a) देते हैं।

तो, एक भाग निकले प्रकार चर होता है आप एक प्रकार एक परिमाणक कि GHC infers कि परिमाणक के दायरे बाहर एक अनिर्धारित प्रकार के साथ एकीकृत किया जाना चाहिए से बंधे है जब।

---

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

मैं पूरी तरह यकीन है कि जहाँ शब्द से उत्पन्न नहीं कर रहा हूँ, लेकिन मैं इसे Skolem normal form और सार्वभौमिक के मामले में अस्तित्व मात्रा का प्रतिनिधित्व शामिल है, के रूप में GHC में किया जाता है लगता है कि होगा। एक स्कोलम (या कठोर) प्रकार चर एक है, कुछ गुंजाइश के भीतर, किसी कारण के लिए एक अज्ञात-लेकिन-विशिष्ट प्रकार है - एक विद्युतीय डेटा प्रकार, & सी से आने वाले पॉलिमॉर्फिक प्रकार का हिस्सा होना।

Answer 2

जैसा कि मैं इसे समझता हूं, एक "स्कोलम चर" एक चर है जो किसी भी अन्य चर से मेल नहीं खाता है।

यह स्पष्ट रूप से स्पष्ट टोल, जीएडीटी, और अन्य प्रकार के सिस्टम एक्सटेंशन जैसी सुविधाओं का उपयोग करते समय हास्केल में पॉप अप लगता है।

उदाहरण के लिए, निम्न प्रकार पर विचार करें:

data AnyWidget = forall x. Widget x => AnyWidget x 

क्या यह कहता है कि आप किसी भी प्रकार कि Widget वर्ग को लागू करता है ले जा सकते हैं, और एक AnyWidget प्रकार में लपेट है। अब, आप इस खोलना करने की कोशिश लगता है:

unwrap (AnyWidget w) = w 

उम, नहीं, तुम ऐसा नहीं कर सकते। क्योंकि, संकलन समय पर, हमें नहीं पता कि w किस प्रकार है, इसलिए इसके लिए सही प्रकार के हस्ताक्षर लिखने का कोई तरीका नहीं है। यहां w का प्रकार AnyWidget से "बच निकला" है, जिसकी अनुमति नहीं है।

जैसा कि मैं इसे समझता हूं, आंतरिक रूप से जीएचसी w को एक प्रकार का स्कोलेम चर देता है, इस तथ्य का प्रतिनिधित्व करने के लिए कि यह बचाना नहीं चाहिए। (यह एकमात्र ऐसा परिदृश्य नहीं है; कुछ अन्य स्थान हैं जहां टाइपिंग समस्याओं के कारण एक निश्चित मूल्य बच नहीं सकता है।)

Answer 3

त्रुटि संदेश पॉप-अप होता है जब एक प्रकार परिवर्तक अपने दायरे से बचने की कोशिश करता है।

मुझे यह पता लगाने में थोड़ी देर लग गई, इसलिए मैं एक उदाहरण लिखूंगा।

{-# LANGUAGE ExistentialQuantification #-} 
data I a = I a deriving (Show) 
data SomeI = forall a. MkSomeI (I a) 

तो अगर हम एक समारोह

unI (MkSomeI i) = i 

GHC इस समारोह टाइप-अनुमान/प्रकार की जाँच करने के लिए मना कर दिया लिखने की कोशिश।

---

क्यों? प्रकार अपने आप को अनुमान लगाने के लिए कोशिश करते हैं:

• unI एक लैम्ब्डा परिभाषा है, इसलिए इसे प्रकार कुछ प्रकार x और y के लिए x -> y है।
• MkSomeI एक प्रकार forall a. I a -> SomeI
  • MkSomeI i एक प्रकार SomeI
  • एलएचएस पर i है कुछ प्रकार z के लिए एक प्रकार I z है है। forall क्वांटिफायर के कारण, हमें नए (ताजा) प्रकार परिवर्तक को पेश करना पड़ा। ध्यान दें, यह सार्वभौमिक नहीं है, क्योंकि यह (SomeI i) अभिव्यक्ति के अंदर बाध्य है।
  • इस प्रकार हम SomeI के साथ प्रकार परिवर्तनीय x को एकीकृत कर सकते हैं, यह ठीक है। तो unI में SomeI -> y होना चाहिए।
• आरएचएस पर i इस प्रकार प्रकार I z भी है।
• इस बिंदु पर यूनिफायर y और I z को एकीकृत करने का प्रयास करता है, लेकिन यह नोट करता है कि z निचले संदर्भ में पेश किया गया है। इस प्रकार यह विफल रहता है।

अन्यथा unI के लिए प्रकार प्रकार forall z. SomeI -> I z होता है, लेकिन सही exists z. SomeI -> I z है। फिर भी एक जीएचसी सीधे प्रतिनिधित्व नहीं कर सकता है।

---

इसी तरह, हम क्यों

data AnyEq = forall a. Eq a => AE a 
-- reflexive :: AnyEq -> Bool 
reflexive (AE x) = x == x 

काम करता है देख सकते हैं।

AE x के अंदर (अस्तित्व में) चर बाहरी क्षेत्र में नहीं बचता है, इसलिए सबकुछ ठीक है।

---

इसके अलावा, मैं GHC 7.8.4 में एक "feature" और 7.10.1 का सामना करना पड़ा जहां RankNTypes पर ही ठीक है, लेकिन GADTs जोड़ने त्रुटि

{-# LANGUAGE RankNTypes #-} 
{-# LANGUAGE GADTs #-} 

example :: String -> I a -> String 
example str x = withContext x s 
    where 
    s i = "Foo" ++ str 

withContext :: I a -> (forall b. I b -> c) -> c 
withContext x f = f x 

तो यह आपके कोड के साथ कुछ भी गलत नहीं हो सकता है चलाता है । यह जीएचसी हो सकता है, जो लगातार सब कुछ नहीं समझ सकता है।

EDIT: समाधान s :: forall a. I a -> String पर एक प्रकार देना है। MonoLocalBinds पर

GADTs बारी है, जो s की अनुमानित प्रकार Skolem चर वाला राज्य बन गया, तो प्रकार नहीं forall a. I a -> String है, लेकिन t -> String, थे t गलत संदर्भ में बाध्य हो जाता है। देखें: https://ghc.haskell.org/trac/ghc/ticket/10644