रैंकेंटाइप्स और पॉलीकिंड्स

Question

f1 और f2 के बीच क्या अंतर है?

$ ghci -XRankNTypes -XPolyKinds 
Prelude> let f1 = undefined :: (forall a  m. m a -> Int) -> Int 
Prelude> let f2 = undefined :: (forall (a :: k) m. m a -> Int) -> Int 
Prelude> :t f1 
f1 :: (forall   (a :: k) (m :: k -> *). m a -> Int) -> Int 
Prelude> :t f2 
f2 :: (forall (k :: BOX) (a :: k) (m :: k -> *). m a -> Int) -> Int 

RankNTypes and scope of forall पर इस प्रश्न से संबंधित। kind polymorphism पर जीएचसी उपयोगकर्ता की मार्गदर्शिका से लिया गया उदाहरण।

Answer 1

f2, तरह k में बहुरूपी होने के लिए, जबकि f1 तरह अपने आप में सिर्फ बहुरूपी है अपने तर्क की आवश्यकता है। तो अगर आप

{-# LANGUAGE RankNTypes, PolyKinds #-} 
f1 = undefined :: (forall a m. m a -> Int) -> Int 
f2 = undefined :: (forall (a :: k) m. m a -> Int) -> Int 
x = undefined :: forall (a :: *) m. m a -> Int 

तो :t f1 x प्रकार ठीक परिभाषित करते हैं, जबकि :t f2 x शिकायत:

*Main> :t f2 x 

<interactive>:1:4: 
    Kind incompatibility when matching types: 
     m0 :: * -> * 
     m :: k -> * 
    Expected type: m a -> Int 
     Actual type: m0 a0 -> Int 
    In the first argument of ‘f2’, namely ‘x’ 
    In the expression: f2 x 

Answer 2

के खूनी बनें। हमें सबकुछ मापना होगा और मात्रा का डोमेन देना होगा। मानों के प्रकार हैं; प्रकार के स्तर की चीजें हैं; BOX में रहते हैं।

f1 :: forall (k :: BOX). 
     (forall (a :: k) (m :: k -> *). m a -> Int) 
     -> Int 

f2 :: (forall (k :: BOX) (a :: k) (m :: k -> *). m a -> Int) 
     -> Int 

अब, न तो उदाहरण के प्रकार में k स्पष्ट रूप से मात्रा निर्धारित किया है, तो GHC चाहे और जहां k उल्लेख किया गया है के आधार पर जहां कि forall (k :: BOX) डाल करने के लिए यह तय करना है, है। मुझे पूरी तरह से यकीन नहीं है कि मैं समझता हूं या नीति के बचाव के लिए तैयार हूं।

Ørjan अभ्यास में अंतर का एक अच्छा उदाहरण देता है। चलो इसके बारे में भी खूनी हो। संबंधित अनुप्रयोग के लिए forall और f @ type से संबंधित अमूर्तता को स्पष्ट करने के लिए मैं /\ (a :: k). t लिखूंगा। गेम यह है कि हमें @ -ed तर्क चुनने के लिए मिलता है, लेकिन हमें शैतान चुनने वाले तर्कों के साथ /\ -ed तर्कों को तैयार करने के लिए तैयार रहना होगा।

हम

x :: forall (a :: *) (m :: * -> *). m a -> Int 

है और उसके अनुसार पता लग सकता है कि f1 x वास्तव में

f1 @ * (/\ (a :: *) (m :: * -> *). x @ a @ m) 

है हालांकि, अगर हम f2 x एक ही इलाज देने की कोशिश, हम देखते हैं

f2 (/\ (k :: BOX) (a :: k) (m :: k -> *). x @ ?m0 @ ?a0) 
?m0 :: * 
?a0 :: * -> * 
where m a = m0 a0 

हास्केल टाइप सिस्टम पूरी तरह सिंटैक्टिक के रूप में टाइप एप्लिकेशन का इलाज करता है, इसलिए एक ही रास्ता है कि समीकरण हल किया जा सकता, कार्यों की पहचान करने और तर्क

(?m0 :: * -> *) = (m :: k -> *) 
(?a0 :: *)  = (a :: k) 

लेकिन उन समीकरणों भी अच्छी तरह से kinded नहीं कर रहे हैं की पहचान करके है, क्योंकि k चुना जाना करने के लिए स्वतंत्र नहीं है: यह /\@ नहीं एड किया जा रहा है -ईडी।

आम तौर पर, इन उबेर-पॉलिमॉर्फिक प्रकारों के साथ पकड़ने के लिए, सभी क्वांटिफ़ायर लिखना अच्छा होता है और फिर पता चलता है कि यह शैतान के खिलाफ आपके गेम में कैसे बदल जाता है। कौन चुनता है, और किस क्रम में। एक तर्क प्रकार के अंदर forall को स्थानांतरित करने से इसके चयनकर्ता बदल जाते हैं, और अक्सर जीत और हार के बीच अंतर बना सकते हैं।

Answer 3

अपने परिभाषा पर f1 स्थानों अधिक प्रतिबंध के प्रकार, जबकि इसकी तर्क पर f2 स्थानों अधिक प्रतिबंध के प्रकार।

यही कारण है: f1 के प्रकार, जबकि f2 के प्रकार के अपने तर्क तरह k में बहुरूपी होने की आवश्यकता है, तरह k में बहुरूपी होने के लिए अपनी परिभाषा की आवश्यकता है।

f1 :: forall (k::BOX). (forall   (a::k) (m::k->*). m a -> Int) -> Int 
f2 ::     (forall (k::BOX) (a::k) (m::k->*). m a -> Int) -> Int 

-- Show restriction on *definition* 
f1 g = g (Just True) -- NOT OK. f1 must work for all k, but this assumes k is * 
f2 g = g (Just True) -- OK 

-- Show restriction on *argument* (thanks to Ørjan) 
x = undefined :: forall (a::*) (m::*->*). m a -> Int 
f1 x -- OK 
f2 x -- NOT OK. the argument for f2 must work for all k, but x only works for *