प्रतिबंधित monoid प्रकार मान रचना

Question

मैं यह है कि Monoid का एक उदाहरण तो मैं अच्छा मूल्यों रचना प्राप्त कर सकते हैं एक डेटा प्रकार है:

data R a = R String (Maybe (String → a)) 

instance Monoid (R a) where 
    mempty = R "" Nothing 
    R s f `mappend` R t g = R (s ++ t) (case g of Just _ → g; Nothing → f) 

इसके बाद, मैं एक दूसरे के साथ सभी R a मूल्यों गठबंधन करने के लिए नहीं करना चाहते, यह मेरे डोमेन में समझ में नहीं आता है।

{-# LANGUAGE DataKinds, KindSignatures #-} 

data K = T1 | T2 
data R (t ∷ K) a = R String (Maybe (String → a)) 

instance Monoid (R t a) where … 

तो मैं "प्रतिबंधित" है मान::

v1 ∷ R T1 Int 
v2 ∷ R T2 Int 
-- v1 <> v2 => type error 

और "अप्रतिबंधित": तो मैं प्रेत प्रकार t परिचय

v ∷ R t Int 
-- v <> v1 => ok 
-- v <> v2 => ok 

लेकिन अब मैं एक समस्या है। यह उदाहरण के लिए, v30 की बात आती है:

• मैं विशाल डेटा तरह घोषणा (data K = T1 | … | T30) होगा। मैं प्रेत प्रकारों के अनंत स्रोत प्राप्त करने के लिए प्रकार के स्तर के प्राकृतिक उपचार का उपयोग करके हल कर सकता हूं (इलाज बीमारी से भी बदतर है, है ना?)
• मुझे याद रखना चाहिए कि किस प्रेत प्रकार का उपयोग करने के लिए निर्भर करता है जब आश्रित में प्रकार हस्ताक्षर लिखते हैं कोड (कि वास्तव में कष्टप्रद है)

वहाँ किसी भी तरह की संरचना को प्रतिबंधित करने के लिए एक आसान दृष्टिकोण है?

Answer 1

ConstrainedMonoid

मैं हाल ही में एक बहुत ही इसी तरह की समस्या के लिए आया था, जो मैं अंत में जिस तरह से इस पोस्ट के अंत में वर्णित हल के लिए खोज रहे (एक monoid को शामिल नहीं है, लेकिन प्रकार पर विधेय का उपयोग)। हालांकि, मैंने चुनौती ली और कक्षा लिखने की कोशिश की।

यहाँ विचार है:

data K = T0 | T1 | T2 | T3 | T4 
data R a (t :: K) = R String (Maybe (String -> a)) 

instance ConstrainedMonoid (R a) where 
    type Compatible (R a) T1 T1 =() 
    type Compatible (R a) T2 T2 =() 
    type Compatible (R a) T3 T3 =() 
    type Compatible (R a) T4 T4 =() 
    type Compatible (R a) T0 y =() 
    type Compatible (R a) x T0 =() 

    type TAppend (R a) T0 y = y 
    type TAppend (R a) x T0 = x 
    type TAppend (R a) T1 T1 = T1 
    type TAppend (R a) T2 T2 = T2 
    type TAppend (R a) T3 T3 = T3 
    type TAppend (R a) T4 T4 = T4 
    type TZero (R a) = T0 

    memptyC = R "" Nothing 
    R s f `mappendC` R t g = R (s ++ t) (g `mplus` f) 

यह दुर्भाग्य से लेता है:

class ConstrainedMonoid m where 
    type Compatible m (t1 :: k) (t2 :: k) :: Constraint 
    type TAppend m (t1 :: k) (t2 :: k) :: k 
    type TZero m :: k 

    memptyC :: m (TZero m) 
    mappendC :: (Compatible m t t') => m t -> m t' -> m (TAppend m t t') 

ठीक है, वहाँ तुच्छ उदाहरण है, जो वास्तव में कुछ भी नया नहीं जोड़ता है (मैं R रों प्रकार तर्क बदली) बहुत सारे अनावश्यक प्रकार के उदाहरण (OverlappingInstances प्रकार परिवारों के लिए काम नहीं करते हैं), लेकिन मुझे लगता है कि यह मान स्तर के साथ-साथ मूल्य स्तर पर, मोनोइड कानूनों को पूरा करता है।

हालांकि, यह बंद नहीं है। यह विभिन्न मोनोइड्स के सेट की तरह है, जो K द्वारा अनुक्रमित है। यदि आप यही चाहते हैं, तो यह पर्याप्त होना चाहिए।

यदि आप चाहते हैं और अधिक

की एक अलग संस्करण पर नजर डालते हैं:

data B (t :: K) = B String deriving Show 

instance ConstrainedMonoid B where 
    type Compatible B T1 T1 =() 
    type Compatible B T2 T2 =() 
    type Compatible B T3 T3 =() 
    type Compatible B T4 T4 =() 

    type TAppend B x y = T1 
    type TZero B = T3 

    memptyC = B "" 
    (B x) `mappendC` (B y) = B (x ++ y) 

यह ऐसा मामला है जो आपके डोमेन में समझ में आता है हो सकता है - हालांकि, यह एक monoid अब और नहीं है। और यदि आपने इसे बनाने की कोशिश की है, तो यह उपरोक्त उदाहरण के समान ही होगा, बस TZero के साथ।मैं वास्तव में यहां अनुमान लगा रहा हूं, लेकिन मेरा अंतर्ज्ञान मुझे बताता है कि केवल वैध मोनोइड उदाहरण R a के समान हैं; केवल अलग इकाई मूल्यों के साथ।

अन्यथा, आप कुछ ऐसे सहयोगी (और शायद एक टर्मिनल ऑब्जेक्ट के साथ, मुझे लगता है) के साथ समाप्त हो जाएगा, जो संरचना के तहत बंद नहीं है। और यदि आप संरचना को K के बराबर प्रतिबंधित करना चाहते हैं, तो आप इकाई मान खो देंगे।

एक बेहतर तरीका (IMHO)

यहाँ कैसे मैं वास्तव में मेरी समस्या हल (मैं भी, उस वक्त monoids नहीं सोचा था, क्योंकि वे भावना किसी भी तरह नहीं था) है। समाधान अनिवार्य रूप से Compatible "बाधा निर्माता" है, जो दो प्रकार पर एक विधेय के रूप में छोड़ दिया जाता है के अलावा सब कुछ बंद स्ट्रिप्स:

type family Matching (t1 :: K) (t2 :: K) :: Constraint 
type instance Matching T1 T1 =() 
type instance Matching T2 T1 =() 
type instance Matching T1 T2 =() 
type instance Matching T4 T4 =() 

तरह

foo :: (Matching a b) => B a -> B b -> B Int 

इस्तेमाल किया यह आप संगतता की अपनी परिभाषा पर पूर्ण नियंत्रण देता , और आप किस तरह की रचना (आवश्यक रूप से monoidal) चाहते हैं, और यह अधिक सामान्य है। यह भी अनंत प्रकार का विस्तार किया जा सकता है:

-- pseudo code, but you get what I mean 
type instance NatMatching m n = (IsEven m, m > n) 

---

अपने दो पिछले अंक का जवाब:

• हां, आप अपने वस्तु के रूप में पर्याप्त रूप से कई प्रकार परिभाषित करने के लिए किया है। लेकिन मुझे लगता है कि उन्हें वैसे भी आत्म-व्याख्या करना चाहिए। आप उन्हें समूहों में भी विभाजित कर सकते हैं, या एक पुनरावर्ती प्रकार को परिभाषित कर सकते हैं।

• आपको मुख्य रूप से इंडेक्स प्रकार के अर्थ को दो स्थानों पर याद दिलाना होगा: बाधा की परिभाषा, और शायद कारखाने के तरीकों (mkB1 :: String -> B T1) के लिए। लेकिन मुझे लगता है कि अगर समस्याएं अच्छी तरह से नामित हैं, तो समस्या नहीं होनी चाहिए। (यह बहुत बेमानी हो सकता है, हालांकि - मैं एक तरह से अभी तक कि से बचने के लिए नहीं मिला है शायद वें काम करेगा।।)

इस आसान हो सकता है?

क्या मैं वास्तव में लिखने के लिए सक्षम होने के लिए चाहते हैं निम्नलिखित:

type family Matching (t1 :: K) (t2 :: K) :: Constraint 
type instance Matching T1 y =() 
type instance Matching x T1 =() 
type instance Matching x y = (x ~ y) 

मुझे डर है कि यह एक गंभीर कारण अनुमति दी जानी करने के लिए नहीं है; हालांकि, शायद, यह अभी लागू नहीं किया गया है ...

संपादित करें: आजकल, हमारे पास closed type families है, जो वास्तव में ऐसा करता है।