वैध फॉरल प्रकार को एक लेट-बाउंड वैरिएबल

Question

पर लिखने में त्रुटि टाइप करें क्या यह प्रकार चेकर में एक बग है?

Prelude> let (x :: forall a. a -> a) = id in x 3 

<interactive>:0:31: 
    Couldn't match expected type `forall a. a -> a' 
       with actual type `a0 -> a0' 
    In the expression: id 
    In a pattern binding: (x :: forall a. a -> a) = id 

तथ्य यह है कि इसके बाद के संस्करण प्रकार की जांच करने में विफल रहता है, लेकिन इस विकृति सफल होता है:

Prelude> let (x :: (forall a. a -> a) -> Int) = (\f -> f 3) in x id 
3 

मुझे सुराग को लगता है कि "कमजोर prenex रूपांतरण" (this paper का पेज 23 देखें) किसी भी तरह संबंधित हो सकती है । एक forall को एक विरोधाभासी स्थिति में एम्बेड करना जहां इसे "फ़्लोट आउट" नहीं किया जा सकता है, यह इस अजीब त्रुटि से सुरक्षित रखने के लिए प्रतीत होता है।

Answer 1

मुझे लगता है कि यहां क्या हो रहा है यह है: मानक दामा – मिलनर प्रकार अनुमान, बाइंडिंग एकमात्र ऐसा स्थान है जहां एक प्रकार का सामान्यीकरण होता है। आपके असफल उदाहरण का उपयोग करने वाला प्रकार हस्ताक्षर pattern type signature है जो "स्पष्ट तरीके से पैटर्न के प्रकार को बाधित करता है"। अब, इस उदाहरण में, यह "स्पष्ट" नहीं है कि क्या यह बाधा सामान्यीकरण से पहले या बाद में होनी चाहिए, लेकिन आपका असफल उदाहरण दर्शाता है, मुझे लगता है कि यह सामान्यीकरण से पहले लागू होता है।

अधिक वस्तुतः रखो: एक लेट बाइंडिंग let x = id in ... में, कि id क्या होता है रों प्रकार और फिर forall a0. a0 -> a0 के रूप में सामान्यीकृत है के प्रकार forall a. a->a एक मोनोटाइप में instantiated हो जाता है, a0 -> a0 है, जो तब के रूप में x असाइन किया गया है कहते हैं '। यदि, जैसा कि मुझे लगता है, पैटर्न प्रकार हस्ताक्षर सामान्यीकरण से पहले चेक किया गया है, यह अनिवार्य रूप से संकलक को यह सत्यापित करने के लिए कह रहा है कि मोनोटाइप a0 -> a0 पॉलीटाइप forall a. a -> a से अधिक सामान्य है, जो यह नहीं है।

यदि हम प्रकार के हस्ताक्षर को बाध्यकारी स्तर पर ले जाते हैं, let x :: forall a. a-> a; x = id in ... सामान्यीकरण के बाद हस्ताक्षर की जांच की जाती है (क्योंकि इसे पॉलीमोर्फिक रिकर्सन को सक्षम करने के लिए स्पष्ट रूप से अनुमति दी जाती है), और कोई भी प्रकार त्रुटि उत्पन्न नहीं होती है।

चाहे यह एक बग है या नहीं, मुझे लगता है, राय की बात है। ऐसा लगता है कि एक वास्तविक कल्पना नहीं है जो हमें बताएगी कि यहां सही व्यवहार क्या है; केवल हमारी उम्मीदें हैं। मैं जीएचसी लोगों के साथ इस मामले पर चर्चा करने का सुझाव दूंगा।

Answer 2

वास्तविक जवाब नहीं है, लेकिन एक टिप्पणी के लिए बहुत लंबा है:
यह एक बग भी हो सकता है। अभिव्यक्ति के साथ थोड़ा सा बजाना, असुरक्षित रूप से

let x :: forall a. a -> a; x = id in x 3 

स्पष्ट फ़ॉल्स लिखने पर काम करता है। हालांकि, यह एक बोग-मानक रैंक 1 प्रकार है। कुछ अन्य भिन्नता:

$ ghci-6.12.3 -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables 
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3 
3 

ठीक है, यह काम करता है, मुझे नहीं पता कि लैम्ब्डा अलग तरीके से क्यों व्यवहार करता है, लेकिन ऐसा करता है। हालांकि:

$ ghci -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables 
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3 

<interactive>:0:31: 
    Couldn't match expected type `t0 -> t1' 
       with actual type `forall a. a -> a' 
    The lambda expression `\ y -> id y' has one argument, 
    but its type `forall a. a -> a' has none 
    In the expression: \ y -> id y 
    In a pattern binding: (x :: forall a. a -> a) = \ y -> id y 

(7.2.2; 7.0.4 एक ही त्रुटि देता है)। यह आश्चर्यजनक है।