प्रेत प्रकारों को परिभाषित करना - उदाहरणों को संकलित नहीं कर सकते

Question

मैं प्रेत प्रकारों के बारे में अधिक जानने की कोशिश कर रहा हूं। मैं राल्फ हिनज द्वारा Fun with Phantom Types के माध्यम से पढ़ने की कोशिश कर रहा हूं। वह एक कीवर्ड with का उपयोग कर रहा है मैंने पहले नहीं देखा है और मैं संकलन नहीं कर सकता। जब मैं कोशिश करता हूं तो मुझे = पर एक पार्स त्रुटि मिलती है।

data Type t = RInt     with t = Int 
      | RChar     with t = Char 
      | RList (Type a)   with t = [a ] 
      | RPair (Type a) (Type b) with t = (a, b) 

अखबार में इससे पहले, वह कहता है कि "के साथ" बयान, सख्ती से आवश्यक नहीं हैं आप a = t बजाय सेट कर सकते हैं कि, लेकिन मैं समझ नहीं उनके बिना इस डेटा प्रकार परिभाषित करने के लिए कैसे। निम्नलिखित त्रुटियों के साथ: Not in scope: type variable 'a'

data Type t = RInt 
      | RChar 
      | RList (Type a) 
      | RPair (Type a) (Type b) 

मुझे क्या याद आ रही है?

Answer 1

मेरा अनुमान है कि परिभाषा sans- with पत्र में सुझाव दिया

data Type t = RInt 
      | RChar 
      | RList (Type t) 
      | RPair (Type t) (Type t) 

से ऊपर है, पैरामीटर t इस्तेमाल कभी नहीं किया है। यह वास्तव में प्रेत है।

इसका तात्पर्य है कि, उदाहरण के लिए

RInt :: Type a 

के लिए किसी भी प्रकार a। इसके विपरीत, यदि with बाधाओं का पालन किया गया था, तो RInt :: Type t किसी भी टी के लिए लेकिन t ~ Int के लिए असंभव होगा।

with वाक्यविन्यास जीएचसी में मौजूद नहीं है, लेकिन जीएडीटी अनिवार्य रूप से एक ही भूमिका निभाते हैं।

{-# LANGUAGE GADTs #-} 
data Type t where 
    RInt :: t ~ Int => Type t 
    RChar :: t ~ Char => Type t 
    RList :: t ~ [a] => Type a -> Type t 
    RPair :: t ~ (a,b) => Type a -> Type b -> Type t 

नोट कैसे with प्रत्येक निर्माता में एक समानता बाधा बन जाता है। यह मूल रूप से वही बात है, जो अलग-अलग लिखी गई है।

अधिक दृढ़तापूर्वक, हम

data Type t where 
    RInt :: Type Int 
    RChar :: Type Char 
    RList :: Type a -> Type [a] 
    RPair :: Type a -> Type b -> Type (a,b) 

में ऊपर पुनर्लेखन कर सकते हैं जहां की कमी की गई "inlined" है अंतिम प्रकार में।

Answer 2

हालांकि बदसूरत, निम्नलिखित काम करेंगे और भावना में उस संकेत के करीब थोड़ा समझा जा सकता है। यह अनिवार्य रूप से एक प्रकार के जीएडीटी को टाइप इक्विटी में desugaring (जो कि अपने स्वयं के एक्सटेंशन नहीं लग रहा है, तो आपको या तोGADTs या TypeFamilies उन्हें उपयोग करने में सक्षम) और अस्तित्व के लिए आवश्यक है।

{-# LANGUAGE ExistentialQuantification, TypeFamilies #-} 

data Type t = t ~ Int => RInt 
      | t ~ Char => RChar 
      | forall a. t ~ [a] => RList (Type a) 
      | forall a b. t ~ (a, b) => RPair (Type a) (Type b)