एक जीएडीटी फॉर्मेटेड एएसटी में हेटरोजेनस संग्रह के प्रकार को कैसे निर्दिष्ट करें?

Question

मैं एक गतिशील भाषा के लिए एक टाइप एएसटी बनाना चाहता हूं। वर्तमान में, मैं संग्रहों को संभालने पर फंस गया हूं। मैं List काफी अच्छी तरह से की घटनाओं को निर्माण कर सकते हैं जबकि

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE ExistentialQuantification #-} 

data Box = forall s. B s 

data BinOp = Add | Sub | Mul | Div 
      deriving (Eq, Show) 

data Flag = Empty | NonEmpty 

data List :: Flag -> * -> * where 
    Nil :: List Empty a 
    Cons :: a -> List f a -> List NonEmpty a 

data Expr ty where 
    EInt :: Integer -> Expr Integer 
    EDouble :: Double -> Expr Double 
-- EList :: List -> Expr List 

:

*Main> :t (Cons (B (EInt 1)) (Cons (B (EDouble 2.0)) Nil)) 
(Cons (B (EInt 1)) (Cons (B (EDouble 2.0)) Nil)) 
    :: List Box 'NonEmpty 

मैं बिल्कुल यकीन है कि EList के लिए Expr में इस प्रकार के सांकेतिक शब्दों में बदलना करने के लिए कैसे नहीं कर रहा हूँ यहाँ एक प्रतिनिधि कोड नमूना है। क्या मैं यहां पर सही रास्ते पर भी हूं?

Answer 1

इस समस्या से संपर्क करने का एक तरीका रन-टाइम प्रकार के प्रतिनिधियों के साथ मूल्यों को टैग करना है। मैं यहां स्टेफनी वीरिच का प्रसारण कर रहा हूं। चलो एक छोटा सा उदाहरण है। सबसे पहले, कुछ प्रकार के लिए एक प्रतिनिधित्व दें। यह आमतौर पर सिंगलटन निर्माण के साथ किया जाता है।

data Type :: * -> * where 
    Int :: Type Int 
    Char :: Type Char 
    List :: Type x -> Type [x] 

तो Type Int क्योंकि यह प्रकार Int के रन-टाइम प्रतिनिधि के रूप में कार्य करता है, एक मूल्य है, जो मैं भी Int बुलाया गया है शामिल हैं। यदि आप मोनोक्रोम चीजों में भी रंग देख सकते हैं, Int:: के बाईं ओर लाल है, और के बाद Int है।

अब हम अस्तित्व पैकेजिंग, उपयोगिता को संरक्षित कर सकते हैं।

data Cell :: * where 
(:::) :: x -> Type x -> Cell 

एक Cell अपनी तरह का एक रन-टाइम प्रतिनिधि के साथ टैग एक मूल्य है। आप अपने प्रकार के टैग को पढ़कर मूल्य की उपयोगिता को पुनर्प्राप्त कर सकते हैं। दरअसल, जैसा कि प्रकार प्रथम क्रम संरचनाएं हैं, हम उन्हें समान तरीके से समानता के लिए जांच सकते हैं।

data EQ :: k -> k -> * where 
    Refl :: EQ x x 

typeEQ :: Type x -> Type y -> Maybe (EQ x y) 
typeEQ Int Int = Just Refl 
typeEQ Char Char = Just Refl 
typeEQ (List s) (List t) = case typeEQ s t of 
    Just Refl -> Just Refl 
    Nothing -> Nothing 
typeEQ _ _ = Nothing 

प्रकार प्रतिनिधियों पर एक बूलियन समानता किसी काम का नहीं है: हम समानता परीक्षण की जरूरत है सबूत कि प्रतिनिधित्व किया प्रकार एकीकृत किया जा सकता है के निर्माण के लिए। सबूत-उत्पादन परीक्षण के साथ, हम

gimme :: Type x -> Cell -> Maybe x 
gimme t (x ::: s) = case typeEQ s t of 
    Just Refl -> Just x 
    Nothing -> Nothing 

बेशक, प्रकार टैग लिखना एक उपद्रव है। लेकिन कुत्ते को क्यों रखें और खुद को छाल क्यों करें?

class TypeMe x where 
    myType :: Type x 

instance TypeMe Int where 
    myType = Int 

instance TypeMe Char where 
    myType = Char 

instance TypeMe x => TypeMe [x] where 
    myType = List myType 

cell :: TypeMe x => x -> Cell 
cell x = x ::: myType 

और अब हम जैसे

myCells :: [Cell] 
myCells = [cell (length "foo"), cell "foo"] 

कर सकते हैं और फिर

> gimme Int (head myCells) 
Just 3 

बेशक

मिलता है, यह सब अगर हम ऐसा करने के लिए नहीं था इसलिए बहुत tidier होगा सिंगलटन निर्माण और ऐसे प्रकारों पर पैटर्न-मिलान कर सकता है क्योंकि हम रन-टाइम पर बनाए रखना चुन सकते हैं। मुझे आशा है कि हम वहां पहुंच जाएंगे जब पौराणिक pi क्वांटिफायर कम पौराणिक हो जाता है।