प्रकार निष्कर्ष - a0

Question

चलें कहते हैं कि मैं इस कार्यक्रम

{-# LANGUAGE GADTs #-} 

data My a where 
    A :: Int -> My Int 
    B :: Char -> My Char 


main :: IO() 
main = do 
    let x = undefined :: My a 

    case x of 
    A v -> print v 

    -- print x 

ठीक संकलित है अछूत है।

लेकिन जब मैं print x में टिप्पणी, मैं मिलता है:

gadt.hs: line 13, column 12: 
    Couldn't match type ‘a0’ with ‘()’ 
    ‘a0’ is untouchable 
     inside the constraints (a1 ~ GHC.Types.Int) 
     bound by a pattern with constructor 
       Main.A :: GHC.Types.Int -> Main.My GHC.Types.Int, 
       in a case alternative 
     at /home/niklas/src/hs/gadt-binary.hs:13:5-7 
    Expected type: GHC.Types.IO a0 
    Actual type: GHC.Types.IO() 
    In the expression: System.IO.print v 
    In a case alternative: Main.A v -> System.IO.print v 

मैं लाइन 13 (A v -> print v) में इस त्रुटि क्यों मिलता है केवल print x लाइन में के बजाय?

मैंने सोचा कि पहली घटना प्रकार को निर्धारित करना चाहिए।

कृपया मुझे प्रबुद्ध :)

Answer 1

ठीक है, पहले ध्यान दें कि इस विशेष print x साथ कोई संबंध नहीं है: जब उदा main समाप्त होने आप एक ही त्रुटि मिलती है putStrLn "done"।

तो समस्या मामला ब्लॉक में वास्तव में, एक do की कि केवल पिछले बयान में अर्थात् do ब्लॉक के हस्ताक्षर के प्रकार करने के लिए आवश्यक है। अन्य बयान केवल उसी मोनैड में होना चाहिए, यानी IO a0IO() के बजाय।

अब, आम तौर पर इस a0 बयान से ही, मान लिया जाता है तो उदाहरण के लिए आप

do getLine 
    putStrLn "discarded input" 

हालांकि getLine :: IO String बजाय IO() लिख सकते हैं। हालांकि, आपके उदाहरण में जानकारी print :: ... -> IO()case ब्लॉक, के अंदर से एक GADT मैच से आता है। और ऐसे जीएडीटी मैचों में अन्य हास्केल स्टेटमेंट्स से भिन्न व्यवहार होता है: मूल रूप से, वे किसी भी प्रकार की जानकारी को अपने दायरे से बचने नहीं देते हैं, क्योंकि यदि जानकारी जीएडीटी कन्स्ट्रक्टर से आई है तो यह case के बाहर सही नहीं है।

कि विशिष्ट उदाहरण में, यह काफी स्पष्ट a0 ~() GADT मैच से a1 ~ Int से कोई लेना देना कुछ भी नहीं है कि लगता है, लेकिन सामान्य रूप में, इस तरह के एक तथ्य ही सिद्ध किया जा सकता है अगर GHC सभी प्रकार की जानकारी जहां के लिए का पता लगाया यह से आया था। मुझे नहीं पता कि यह भी संभव है, यह निश्चित रूप से हास्केल की हिंडली-मिलनर प्रणाली से अधिक जटिल होगा, जो पर प्रकार की जानकारी को एकीकृत करता है, जो अनिवार्य रूप से मानता है कि इससे कोई फर्क नहीं पड़ता कि जानकारी कहां से आई है।

इसलिए, GADT बस एक कठोर “ प्रकार की जानकारी डायोड ” के रूप में कार्य से मेल खाता है: सामान अंदर बाहर की दुनिया में प्रकार निर्धारित करने के लिए, जैसे कि एक पूरे के रूप case ब्लॉक IO() होना चाहिए कभी नहीं किया जा सकता।

हालांकि, अगर आप मैन्युअल रूप से जोर कर सकते हैं, बल्कि बदसूरत

(case x of 
    A v -> print v 
    ) :: IO() 

साथ या

() <- case x of 
      A v -> print v