हास्केल: यह टाइप-चेक क्यों करता है?

Question

यह प्रतिबिंब-0.5 से लिया गया एक न्यूनतम उदाहरण है।

>:t Zero 
Zero :: Zero -> Zero 

यह समझ में आता है: मैं निर्माता है जो एक शून्य लेता है और एक शून्य रिटर्न के प्रकार के लिए पूछ रहा हूँ

{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-} 
{-# OPTIONS_GHC -fno-cse -fno-full-laziness -fno-float-in #-} 

import Control.Applicative 
import Data.Proxy 

newtype Zero = Zero Zero deriving (Show) 

class ReifiesNum s where 
    reflectNum :: Num a => proxy s -> a 

instance ReifiesNum Zero where 
    reflectNum = pure 0 

GHCi में, मैं निम्नलिखित मिलता है।

>:t reflectNum 
reflectNum :: (ReifiesNum s, Num a) => proxy s -> a 

यह भावना है कि मैं की तरह

>let x = Just (undefined::Zero) 
>reflectNum x 

क्योंकि प्रकार बस शून्य से मेल खाता प्रकार चर 'प्रॉक्सी s' कुछ लिख सकता है बनाता है।

अंत में, भ्रामक हिस्सा:

>:t (reflectNum Zero) 
(reflectNum Zero) :: Num a => a 

मुझे समझ नहीं आता कैसे निर्माता शून्य :: शून्य के प्रकार -> शून्य जाहिरा तौर पर मेल खाता प्रकार चर 'प्रॉक्सी s', लेकिन जाहिरा तौर पर इसकी वजह करता है प्रकार (reflectNum शून्य) सिर्फ 'ए' है।

मैं इस उदाहरण को समझने में सहायता की सराहना करता हूं, और प्रासंगिक अवधारणाओं के लिंक की सराहना की जाएगी।

धन्यवाद

Answer 1

यह आप बंद फेंकने समारोह तीर का सिर्फ इन्फ़िक्स वाक्य रचना है। सबसे पहले, यहां एक आसान समझने वाला मामला है: Maybe Int। यह proxy s से मेल बनाने के लिए हम सिर्फ सेट:

proxy = Maybe 
s = Int 

अब a -> b बजाय Fun a b लिखा है, और इसलिए Zero टाइप है Fun Zero Zero (अर्थात (Fun Zero) Zero) का नाटक करते हैं। यह proxy s से मेल बनाने के लिए हम सेट:

proxy = Fun Zero 
s = Zero 

हकीकत में, proxy(->) Zero है, और इसलिए proxy s((->) Zero) Zero ≡ (->) Zero Zero ≡ Zero -> Zero है।