टाइप-इंडेक्स किए गए जीएडीटी

Question

में फॉरल के बारे में उलझन में 'दयालु' मैंने जीएचसी 8.0.1 में एक अनुक्रमित स्थिति में भाग लिया है जिसमें टाइप-इंडेक्स (?) जीएडीटी हैं, जहां प्रकार बनाम हस्ताक्षरों में पहल शुरू करने से विभिन्न प्रकार की जांच होती है व्यवहार।

पर विचार करें निम्न डेटा प्रकारों:

{-# LANGUAGE TypeInType, GADTs, ExplicitForAll #-} 
-- Same thing happens when we replace ExplicitForAll with ScopedTypeVariables 

import Data.Kind 

data F (k :: * -> *) where 

data G :: F k -> * where 
    G :: G x 

यह डेटा प्रकार ठीक संकलित करता है। हालांकि, अगर हम G में x के प्रकार को निर्दिष्ट करना चाहते हैं, तो हमें एक प्रकार की त्रुटि मिलती है।

data H :: F k -> * where 
    H :: forall k' (x :: F k'). H x 

त्रुटि संदेश

• Kind variable ‘k’ is implicitly bound in datatype 
    ‘H’, but does not appear as the kind of any 
    of its type variables. Perhaps you meant 
    to bind it (with TypeInType) explicitly somewhere? 
• In the data declaration for ‘H’ 

हम तरह हस्ताक्षर (साथ या निर्माता में forall के बिना) के लिए forall जोड़ देते हैं तो है, वहाँ कोई त्रुटि है।

data I :: forall k. F k -> * where 
    I :: I x 

data J :: forall k. F k -> * where 
    J :: forall k' (x :: F k'). J x 

क्या चल रहा है?

Answer 1

TypeInType के लेखक यहां। के ए बुहर इसे ऊपर से प्राप्त करता है; यह सिर्फ एक बग है। यह सिर में तय है।

ज्यादा उत्सुक के लिए: यह त्रुटि संदेश जहां

data Proxy (a :: k) = Proxy 

Data.Proxy से आयात किया जा सकता है जैसे

data J = forall (a :: k). MkJ (Proxy a) 

परिभाषाओं को खत्म करने के लिए है। हास्केल 9 8-शैली सिंटैक्स में डेटाटाइप घोषित करते समय, किसी भी अस्तित्व में क्वांटिफाइड चर को स्पष्ट रूप से forall के साथ दायरे में लाया जाना चाहिए। लेकिन k स्पष्ट रूप से कभी भी दायरे में नहीं लाया गया है; यह सिर्फ a के प्रकार में प्रयोग किया जाता है। तो इसका मतलब है कि k को सार्वभौमिक रूप से प्रमाणित किया जाना चाहिए (दूसरे शब्दों में, यह J पर k पैरामीटर जैसे Proxy) पर अदृश्य पैरामीटर होना चाहिए ... लेकिन फिर जब हम J लिखते हैं, तो यह निर्धारित करने का कोई तरीका नहीं है कि k क्या होना चाहिए , तो यह हमेशा संदिग्ध होगा। (इसके विपरीत, हम k पैरामीटर के लिए विकल्प Proxy को a की तरह को देखकर पता लगा सकते हैं।)

J के लिए यह परिभाषा 8.0.1 में और सिर में अनुमति नहीं है।