प्रतिबिंबित इस रहस्यमय हास्केल प्रकार त्रुटि का कारण क्या है?

Question

मैं हास्केल reflection पैकेज के साथ खेल रहा था, और मैं एक प्रकार की त्रुटि में भाग गया जो मैं पूरी तरह समझ नहीं पा रहा हूं।

{-# LANGUAGE TypeApplications #-} 

reifyGood :: (forall s. Reifies s a => Proxy a) ->() 
reifyGood p = reify undefined (\(_ :: Proxy t) -> p @t `seq`()) 

दिलचस्प बात यह है, तथापि, यह थोड़ा अलग कार्यक्रम करता नहीं typecheck:

reifyBad :: (forall s. Reifies s s => Proxy s) ->() 
reifyBad p = reify undefined (\(_ :: Proxy t) -> p @t `seq`()) 

• Could not deduce (Reifies s s) arising from a use of ‘p’ 
    from the context: Reifies s a0 
    bound by a type expected by the context: 
       Reifies s a0 => Proxy s ->() 
• In the first argument of ‘seq’, namely ‘p @t’ 
    In the expression: p @t `seq`() 
    In the second argument of ‘reify’, namely 
    ‘(\ (_ :: Proxy t) -> p @t `seq`())’ 

प्रथम, मैं निम्नलिखित समारोह है, जो खुशी से typechecks लिखने का प्रयास किया अभिव्यक्ति समान हैं, लेकिन प्रकार हस्ताक्षर के बीच अंतर ध्यान दें:

reifyGood :: (forall s. Reifies s a => Proxy a) ->() 
reifyBad :: (forall s. Reifies s s => Proxy s) ->() 

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

reifyBad' :: (forall s. Reifies s s => Proxy s) ->() 
reifyBad' p = reify undefined (\(_ :: Proxy t) -> p @t) `seq`() 

• Couldn't match expected type ‘t0’ with actual type ‘Proxy s’ 
    because type variable ‘s’ would escape its scope 
    This (rigid, skolem) type variable is bound by 
    a type expected by the context: 
     Reifies s a0 => Proxy s -> t0 
• In the expression: p @t 
    In the second argument of ‘reify’, namely 
    ‘(\ (_ :: Proxy t) -> p @t)’ 
    In the first argument of ‘seq’, namely 
    ‘reify undefined (\ (_ :: Proxy t) -> p @t)’ 

तो शायद कुछ और यहाँ खेलने पर है।

reify के प्रकार की जांच करना, यह एक छोटे स्पष्ट हो जाता है कि कुछ गड़बड़ है:

reify :: forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r 

a और s का स्कोप, स्पष्ट रूप से अलग हैं तो यह है कि GHC उन्हें अनुमति नहीं होगी समझ बनाने के लिए लगता है एकजुट। हालांकि, ऐसा लगता है कि Reifies पर कार्यात्मक निर्भरता द्वारा पेश की गई स्थानीय समानता बाधा के बारे में कुछ ऐसा लगता है जो किसी प्रकार का अजीब व्यवहार करता है। दिलचस्प बात यह है कार्यों typechecks की यह जोड़ी:

foo :: forall a r. Proxy a -> (forall s. (s ~ a) => Proxy s -> r) -> r 
foo _ f = f Proxy 

bar :: (forall a. Proxy a) ->() 
bar p = let p' = p in foo p' (\(_ :: Proxy s) -> (p' :: Proxy s) `seq`()) 

... लेकिन foo के प्रकार के हस्ताक्षर में समानता बाधा को दूर करने के लिए उन्हें typecheck करने में विफल है, एक Skolem भागने त्रुटि उत्पादन: इस बिंदु पर

• Couldn't match type ‘a0’ with ‘s’ 
    because type variable ‘s’ would escape its scope 
    This (rigid, skolem) type variable is bound by 
    a type expected by the context: 
     Proxy s ->() 
    Expected type: Proxy s 
    Actual type: Proxy a0 
• In the first argument of ‘seq’, namely ‘(p' :: Proxy s)’ 
    In the expression: (p' :: Proxy s) `seq`() 
    In the second argument of ‘foo’, namely 
    ‘(\ (_ :: Proxy s) -> (p' :: Proxy s) `seq`())’ 

, मैं परेशान हूँ। मेरे पास एक जोड़े (अत्यधिक संबंधित) प्रश्न हैं।

1. reifyBad पहली जगह में typecheck को क्यों असफल रहा है?

2. अधिक विशेष रूप से, यह अनुपलब्ध उदाहरण त्रुटि क्यों उत्पन्न करता है?

इसके अलावा, इस व्यवहार की उम्मीद है और अच्छी तरह से परिभाषित, या यह महज typechecker कि इस विशेष परिणाम उपज होता है का एक अजीब किनारे मामला है?

Answer 1

reify :: forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r 

Skolem आवश्यकता अनिवार्य रूप से कहा गया है कि प्रकार में r ऊपर s जो दूसरा तर्क में मात्रा निर्धारित किया जा रहा है पर निर्भर नहीं कर सकते हैं। अन्यथा, वास्तव में यह reifyr रिटर्न के बाद से अपने दायरे से बच जाएगा।

reifyBad :: (forall s. Reifies s s => Proxy s) ->() 
reifyBad p = reify undefined (\(_ :: Proxy t) -> p @t `seq`()) 

में हम देखते हैं कि reify का दूसरा तर्क \(_ :: Proxy t) -> p @t `seq`() है, इसलिए प्रकार r कि समारोह है, जो () है की वापसी प्रकार होगा। चूंकि r ~()s पर निर्भर नहीं है, यहां कोई भागने की समस्या नहीं है।

हालांकि, p @tp के प्रकार के अनुसार Reifies t t की आवश्यकता है। reifyt ~ s का चयन करेगा, बाधा Reifies s s के समान है। इसके बजाय, reify केवल Reifies s a प्रदान करता है जहां aundefined का प्रकार है।

सूक्ष्म यहां मुद्दा यह है कि, जबकि undefined किसी भी प्रकार a उत्पादन कर सकते हैं, प्रकार चेकर s और a को एकजुट नहीं कर सकता है। ऐसा इसलिए है क्योंकि reify के समान प्रकार के फ़ंक्शन को एक निश्चित (कठोर) प्रकार a का केवल एक मान प्राप्त करने का हकदार है, और उसके बाद इच्छित प्रकार s चुनें। एक a के साथ ऐसे सभी s एस को एकजुट करना गलत होगा, प्रभावी रूप से s की reify की पसंद को बाधित करेगा।

इसके बजाय, संस्करण

reifyBad' :: (forall s. Reifies s s => Proxy s) ->() 
reifyBad' p = reify undefined (\(_ :: Proxy t) -> p @t) `seq`() 

यहाँ r

में \(_ :: Proxy t) -> p @t की वापसी प्रकार है, जो Proxy t, जहां t ~ s है होने के लिए मान लिया जाता है। चूंकि r ~ Proxy ss पर निर्भर करता है, इसलिए हम स्कोलम त्रुटि को ट्रिगर करते हैं।