हास्केल में लंबाई एनोटेट सूचियों का उपयोग कैसे करें

Question

जाहिर है, कुछ GHC एक्सटेंशन के साथ यह संभव है सूची का एक प्रकार है कि लंबाई प्रकार में एन्कोड किया गया है, इस तरह परिभाषित करने के लिए:

{-# LANGUAGE GADTs, EmptyDataDecls #-} 

data Z 
data S a 

data List l a where 
    Nil :: List Z a 
    Cons :: a -> List l a -> List (S l) a 

जबकि मैं देख रहा हूँ क्यों इस कर सकते हैं उपयोगी हो, मुझे वास्तव में इसका उपयोग करने में परेशानी है।

कोई ऐसी सूची कैसे बना सकता है? (इसे प्रोग्राम में हार्डकोडिंग के अलावा।)

कहें कि कोई ऐसा प्रोग्राम बनाना चाहता है जो टर्मिनल से दो ऐसी सूचियों को पढ़ता है और उनके डॉट उत्पाद की गणना करता है। हालांकि वास्तविक गुणात्मक कार्य को कार्यान्वित करना आसान है, प्रोग्राम डेटा को कैसे पढ़ सकता है?

क्या आप मुझे इन तकनीकों का उपयोग करने वाले कुछ मौजूदा कोड पर इंगित कर सकते हैं?

Answer 1

आपको सूची की लंबाई को हार्ड-कोड करने की आवश्यकता नहीं है;

data UList a where 
    UList :: Nat n => List n a -> UList a 

जहां

class Nat n where 
    asInt :: n -> Int 

instance Nat Z where 
    asInt _ = 0 

instance Nat n => Nat (S n) where 
    asInt x = 1 + asInt (pred x) 
     where 
     pred = undefined :: S n -> n 

और हम भी है

fromList :: [a] -> UList a 
fromList [] = UList Nil 
fromList (x:rest) = 
    case fromList rest of 
     UList xs -> UList (Cons x xs) 

इस सेटअप आप सूचियों जिनकी लंबाई संकलन समय पर नहीं जाना जाता है बनाने के लिए अनुमति देता है: के बजाय, आप निम्न प्रकार परिभाषित कर सकते ; आप अस्तित्व वाले रैपर से प्रकार निकालने के लिए case पैटर्न मिलान करके लंबाई तक पहुंच सकते हैं, और फिर प्रकार को पूर्णांक में बदलने के लिए Nat कक्षा का उपयोग करें।

आपको आश्चर्य हो सकता है कि एक प्रकार का लाभ क्या है जिसे आप संकलन समय के मूल्य को नहीं जानते हैं; जवाब यह है कि यद्यपि आप नहीं जानते कि प्रकार क्या होगा, फिर भी आप इनवेरिएंट को लागू कर सकते हैं। उदाहरण के लिए, निम्न कोड सूची की लंबाई को बदल नहीं करने के लिए गारंटी है: अगर हम, कहा जाता है कहते हैं एक प्रकार परिवार, Add का उपयोग कर प्रकार इसके अलावा है, तो हम लिख सकते हैं

mapList :: (a -> b) -> List n a -> List n b 

और

concatList :: List m a -> List n a -> List (Add m n) a 

जो दो सूचियों को जोड़ते हुए आविष्कार को लागू करता है, आपको दो लंबाई के योग के साथ एक नई सूची मिलती है।

Answer 2

आप कड़ी मेहनत से कोड को काफी जरूरत है, के बाद से प्रकार पाठ्यक्रम संकलन समय और GHC प्रकार चेकर के ट्यूरिंग पूर्णता पर तय की है feasibly "अपने आप ही" उन्हें उत्पन्न करने के लिए के साथ दुर्व्यवहार नहीं किया जा सकता। हालांकि, यह नाटकीय नहीं है जैसा कि लगता है: आपको मूल रूप से केवल लंबाई एनोटेशन प्रकार लिखना होगा। बाकी है, विशेष रूप से लंबाई के उल्लेख के बिना किया जा सकता है चारों ओर कुछ अजीब दिखने वर्ग के साथ यद्यपि:

class LOL l where 
    lol :: [a] -> l a 

instance LOL (List Z) where 
    lol _ = Nil 

instance (LOL (List n)) => LOL (List (S n)) where 
    lol (x:xs) = Cons a $ lol xs 
    lol [] = error "Not enough elements given to make requested type length." 

तो फिर तुम सिर्फ

type Four = S(S(S(S Z))) 

get4Vect :: Read a => IO (List Four a) 
get4Vect = lol . read <$> getLine -- For input format [1,2,3,4]. 

---

मैं शान की तरह कुछ का उपयोग कर सकते ' यहां टेम्पलेट हास्केल पर चर्चा नहीं करें, जो निश्चित रूप से संकलन-समय पर स्वचालित रूप से कुछ भी उत्पन्न कर सकता है।

Answer 3

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

उदाहरण के लिए:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE ScopedTypeVariables #-} 

module Lists where 

data Nat = Z | S Nat 

data List l a where 
    Nil :: List Z a 
    Cons :: a -> List n a -> List (S n) a 

data DynList a where 
    DynList :: List l a -> DynList a 

data Refl a b where 
    Refl :: Refl a a 

fromList :: [a] -> DynList a 
fromList []  = DynList Nil 
fromList (x:xs) = cons (fromList xs) where 
    cons (DynList rest) = DynList $ Cons x rest 

toList :: List l a -> [a] 
toList Nil = [] 
toList (Cons x xs) = x : toList xs 

dot :: Num a => List l a -> List l a -> List l a 
dot Nil Nil = Nil 
dot (Cons x xs) (Cons y ys) = Cons (x*y) (dot xs ys) 

haveSameLength :: List l a -> List l' b -> Maybe (Refl l l') 
haveSameLength Nil Nil     = Just Refl 
haveSameLength (Cons _ xs) (Cons _ ys) = case haveSameLength xs ys of 
    Just Refl -> Just Refl 
    Nothing -> Nothing 
haveSameLength _ _      = Nothing 

main :: IO() 
main = do 
    dlx :: DynList Double <- fmap (fromList . read) getLine 
    dly :: DynList Double <- fmap (fromList . read) getLine 

    case (dlx, dly) of 
     (DynList xs, DynList ys) -> case haveSameLength xs ys of 
      Just Refl -> print $ toList $ dot xs ys 
      Nothing -> putStrLn "list lengths do not match" 

यहाँ DynList गतिशील लंबाई की एक सूची है (यानी लंबाई केवल रन-टाइम में जाना जाता है), जो लपेटता एक ठीक से List टाइप किया था। अब, हमारे पास dot फ़ंक्शन है जो दो सूचियों के लिए डॉट उत्पाद की गणना करता है, जिसमें समान लंबाई होती है, इसलिए यदि हम उदाहरण में करते हैं, तो हम स्टडीन से सूचियों को पढ़ते हैं, हमें प्रमाण प्रदान करना होगा कि वास्तव में सूचियों में समान लंबाई है ।

यहां "सबूत" Refl कन्स्ट्रक्टर है। जिस तरह से कन्स्ट्रक्टर घोषित किया गया है इसका मतलब है कि अगर हम मूल्य प्रकार Refl a b के प्रकार a और b समान प्रकार के समान हो सकते हैं। इसलिए हम उत्पादित Refl मान पर प्रकार और पैटर्न मिलान को सत्यापित करने के लिए hasSameLength का उपयोग करते हैं और यह टाइप-चेकर पर्याप्त जानकारी देता है जो इसे दो रन-टाइम सूचियों पर dot पर कॉल करने देता है।

तो इसका अनिवार्य रूप से अर्थ यह है कि टाइप-चेकर हमें कोड को संकलित करने के लिए संकलित समय पर ज्ञात किसी भी सूची की लंबाई को मैन्युअल रूप से सत्यापित करने के लिए मजबूर नहीं करेगा।