गायब होने वाली बाधा का मामला: उच्च रैंक प्रकार

Question

की विषमताएं नीचे वर्णित सभी प्रयोग जीएचसी 8.0.1 के साथ किए गए थे।

यह प्रश्न RankNTypes with type aliases confusion पर एक फॉलो-अप है। मुद्दा वहाँ इस तरह के कार्यों के प्रकार के लिए नीचे उबला हुआ ...

{-# LANGUAGE RankNTypes #-} 

sleight1 :: a -> (Num a => [a]) -> a 
sleight1 x (y:_) = x + y 

... किस प्रकार चेकर द्वारा अस्वीकार कर दिया जाता है ...

ThinAir.hs:4:13: error: 
    * No instance for (Num a) arising from a pattern 
     Possible fix: 
     add (Num a) to the context of 
      the type signature for: 
      sleight1 :: a -> (Num a => [a]) -> a 
    * In the pattern: y : _ 
     In an equation for `sleight1': sleight1 x (y : _) = x + y 

... क्योंकि higher- रैंक बाधा Num acannot be moved outside of the type of the second argument (जैसा कि संभव होगा यदि हमारे पास a -> a -> (Num a => [a]) था)। इसलिए किया जा रहा है, हम एक चर पहले से ही पूरी बात से अधिक मात्रा निर्धारित करने के लिए एक उच्च रैंक बाधा जोड़ने की कोशिश कर अंत यही कारण है, वह यह है कि:

sleight1 :: forall a. a -> (Num a => [a]) -> a 

इस सार-कथन किया के साथ, हम उदाहरण थोड़ा आसान बनाने के लिए कोशिश कर सकते हैं। के कुछ है कि Num की आवश्यकता नहीं है के साथ (+) की जगह है, और परिणाम की कि से समस्या पैदा करने वाले तर्क के प्रकार के संबंध तोड़ देना:

sleight2 :: a -> (Num b => b) -> a 
sleight2 x y = const x y 

यह सिर्फ तरह से पहले (काम नहीं करता त्रुटि में मामूली बदलाव के लिए बचाने के लिए संदेश):

ThinAir.hs:7:24: error: 
    * No instance for (Num b) arising from a use of `y' 
     Possible fix: 
     add (Num b) to the context of 
      the type signature for: 
      sleight2 :: a -> (Num b => b) -> a 
    * In the second argument of `const', namely `y' 
     In the expression: const x y 
     In an equation for `sleight2': sleight2 x y = const x y 
Failed, modules loaded: none. 

यहाँ const का उपयोग करते हुए, हालांकि, शायद अनावश्यक है, इसलिए हम कार्यान्वयन खुद लिखने की कोशिश कर सकता है:

sleight3 :: a -> (Num b => b) -> a 
sleight3 x y = x 

आश्चर्य की बात है, यह वास्तव में काम करता है!

*Main> sleight3 1 "wat" 
1 

मैं कैसे कि सुगम बनाने के लिए के बारे में काफी यकीन नहीं है:

Prelude> :r 
[1 of 1] Compiling Main    (ThinAir.hs, interpreted) 
Ok, modules loaded: Main. 
*Main> :t sleight3 
sleight3 :: a -> (Num b => b) -> a 
*Main> sleight3 1 2 
1 

इससे भी अधिक बिज़ारेलि, वहाँ कोई वास्तविक Num दूसरा तर्क पर बाधा हो रहा है। शायद हम कह सकते हैं, जैसे हम undefined को तब तक जोड़ सकते हैं जब तक हम इसका मूल्यांकन नहीं करते हैं, एक असंतोषजनक बाधा एक प्रकार में बस ठीक हो सकती है जब तक कि इसे दाएं हाथ में कहीं भी एकीकरण के लिए उपयोग नहीं किया जाता है। हालांकि, यह एक बहुत ही कमजोर समानता की तरह लगता है, विशेष रूप से दिया गया है कि गैर-कठोरता के रूप में हम आमतौर पर समझते हैं कि यह मानों को शामिल करने वाली धारणा है, न कि प्रकार। इसके अलावा, यह हमें StringNum b => b के साथ एकीकृत करता है - यह मानते हुए कि ऐसी चीज वास्तव में होती है, जो मुझे बिल्कुल यकीन नहीं है। तो, क्या एक बाधा प्रतीत होता है जब इस तरह से बाधा उत्पन्न होती है, तो क्या एक सटीक वर्णन है?

Answer 1

ओह, यह भी weirder हो जाता है:

Prelude> sleight3 1 ("wat"+"man") 
1 
Prelude Data.Void> sleight3 1 (37 :: Void) 
1 

देखें, वहाँ एक वास्तविक Num कि तर्क पर बाधा है। केवल, क्योंकि (जैसा कि ची पहले से ही टिप्पणी की गई है) b एक कॉन्वेंट स्थिति में है, यह sleight3 पर कॉल करते समय प्रदान करने के लिए एक बाधा नहीं है। इसके बजाय, आप किसी भी प्रकार b चुन सकते हैं, फिर भी जो भी हो, sleight3 इसके लिए Num उदाहरण प्रदान करेगा!

ठीक है, स्पष्ट रूप से यह फर्जी है। sleight3 स्ट्रिंग के लिए ऐसा कोई उदाहरण उदाहरण प्रदान नहीं कर सकता है, और निश्चित रूप से Void के लिए नहीं है। लेकिन यह वास्तव में की आवश्यकता नहीं है क्योंकि, जैसा कि आपने कहा था, जिस तर्क के लिए उस बाधा लागू होगी उसका मूल्यांकन कभी नहीं किया जाता है। याद रखें कि एक बाधा-बहुलक मूल्य अनिवार्य रूप से एक शब्दकोश तर्क का एक कार्य है। sleight3 यह वास्तव में y का उपयोग करने से पहले इस तरह के एक शब्दकोश प्रदान करने का वादा करता है, लेकिन फिर किसी भी तरह से y का उपयोग नहीं करता है, तो यह ठीक है।

यह मूल रूप से इस तरह एक समारोह के साथ के रूप में ही है:

defiant :: (Void -> Int) -> String 
defiant f = "Haha" 

फिर, तर्क समारोह स्पष्ट रूप से संभवतः एक Int उपज नहीं कर सकते हैं क्योंकि वहाँ के साथ यह मूल्यांकन करने के लिए एक Void मूल्य मौजूद नहीं है। लेकिन इसकी आवश्यकता नहीं है, क्योंकि f बस अनदेखा किया जाता है! , const को दूसरा तर्क सिर्फ एक रैंक-0 प्रकार है तो संकलक उस बिंदु पर किसी भी आवश्यक शब्दकोशों को हल करने की जरूरत है:

इसके विपरीत, sleight2 x y = const x y थोड़े sorta y का उपयोग करता है। भले ही const अंततः y दूर फेंकता है, फिर भी यह इस मूल्य के पर्याप्त "बल" को स्पष्ट करता है ताकि यह स्पष्ट हो सके कि यह अच्छी तरह से टाइप नहीं है।