इडिस

Question

में आसान सिंटेक्टिक समानता डेटा प्रकारों के लिए समानता (DecEq) उदाहरण लिखने का कोई आसान तरीका है? उदाहरण के लिए, मैं अपने DecEq घोषणा, जहां ?p कुछ सरल है में हे के लिए निम्नलिखित (एन) लाइनों चाहते हैं:

data Foo = A | B | C | D 

instance [syntactic] DecEq Foo where 
    decEq A A = Yes Refl 
    decEq B B = Yes Refl 
    decEq C C = Yes Refl 
    decEq D D = Yes Refl 
    decEq _ _ = No ?p 

Answer 1

डेविड क्रिश्चियन्सेन कुछ सामान्य रूप में इस स्वचालित करने के लिए काम कर रहा है, और वह अनिवार्य रूप से है ख़त्म होना; यह his GitHub repository में पाया जा सकता है। इस बीच, यहां एक दृष्टिकोण है जो आपको ओ (एन^2) मामलों से इस स्थिति में ओ (एन) मामलों में ले जा सकता है। सबसे पहले, कुछ प्राथमिकताएं। दुर्भाग्य से

IsInjection : (a -> b) -> Type 
IsInjection {a} f = (x,y : a) -> f x = f y -> x = y 

decEqInj : DecEq d => (tToDec : t -> d) -> 
         (isInj : IsInjection tToDec) -> 
         (p, q : t) -> Dec (p = q) 
decEqInj tToDec isInj p q with (decEq (tToDec p) (tToDec q)) 
    | (Yes prf) = Yes (isInj p q prf) 
    | (No contra) = No (\pq => contra (cong pq)) 

, सीधे साबित अपने कार्य एक है: आप डिसाइडेबल समानता के साथ कुछ है, और आप उस प्रकार के लिए अपनी पसंद के प्रकार से एक इंजेक्शन है, तो आप एक निर्णय प्रक्रिया है कि प्रकार के लिए कर सकते हैं इंजेक्शन तुम वापस O (n^2) मामलों के लिए हो जाता है, लेकिन यह मामला है कि एक तर्क के साथ किसी भी समारोह injective है आम तौर पर बताया गया है: इस प्रकार यदि आप डिसाइडेबल साथ एक के लिए अपनी पसंद के प्रकार से एक समारोह है

retrInj : (f : d -> t) -> (g : t -> d) -> 
      ((x : t) -> f (g x) = x) -> 
      IsInjection g 
retrInj f g prf x y gxgy = 
    let fgxfgy = cong {f} gxgy 
     foo = sym $ prf x 
     bar = prf y 
    in trans foo (trans fgxfgy bar) 

समानता और इसके लिए एक पीछे हटाना, तो आपके पास अपने प्रकार के लिए निर्णायक समानता है:

decEqRet : DecEq d => (decToT : d -> t) -> 
      (tToDec : t -> d) -> 
      (isRet : (x : t) -> decToT (tToDec x) = x) -> 
      (p, q : t) -> Dec (p = q) 
decEqRet decToT tToDec isRet p q = 
    decEqInj tToDec (retrInj decToT tToDec isRet) p q 

अंत में, आप आप क्या चुन लिया है के लिए मामलों लिख सकते हैं:

data Foo = A | B | C | D 

natToFoo : Nat -> Foo 
natToFoo Z = A 
natToFoo (S Z) = B 
natToFoo (S (S Z)) = C 
natToFoo _ = D 

fooToNat : Foo -> Nat 
fooToNat A = 0 
fooToNat B = 1 
fooToNat C = 2 
fooToNat D = 3 

fooNatFoo : (x : Foo) -> natToFoo (fooToNat x) = x 
fooNatFoo A = Refl 
fooNatFoo B = Refl 
fooNatFoo C = Refl 
fooNatFoo D = Refl 

instance DecEq Foo where 
    decEq x y = decEqRet natToFoo fooToNat fooNatFoo x y 

नोट natToFoo समारोह कुछ हद तक बड़े पैटर्न है, जबकि, वहाँ नहीं है कि वास्तव में बहुत वहाँ चल रहा है। शायद उन्हें घोंसले से छोटे पैटर्न बनाना संभव हो सकता है, हालांकि यह बदसूरत हो सकता है।

सामान्यीकरण: पहले मैंने सोचा कि यह केवल विशेष मामलों के लिए काम करेगा, लेकिन अब मुझे लगता है कि यह उससे थोड़ा बेहतर हो सकता है। विशेष रूप से, यदि आपके पास क्षैतिज समानता वाले बीजगणित डेटाटाइप होल्डिंग प्रकार हैं, तो आप इसे नेस्टेड Pair के नेस्टेड Either में परिवर्तित करने में सक्षम होना चाहिए, जो आपको वहां ले जाएगा। उदाहरण के लिए (Maybe का उपयोग कर Either (Bool, Nat)() छोटा करने के लिए):

data Fish = Cod Int | Trout Bool Nat | Flounder 

watToFish : Either Int (Maybe (Bool, Nat)) -> Fish 
watToFish (Left x) = Cod x 
watToFish (Right Nothing) = Flounder 
watToFish (Right (Just (a, b))) = Trout a b 

fishToWat : Fish -> Either Int (Maybe (Bool, Nat)) 
fishToWat (Cod x) = Left x 
fishToWat (Trout x k) = Right (Just (x, k)) 
fishToWat Flounder = Right Nothing 

fishWatFish : (x : Fish) -> watToFish (fishToWat x) = x 
fishWatFish (Cod x) = Refl 
fishWatFish (Trout x k) = Refl 
fishWatFish Flounder = Refl 

instance DecEq Fish where 
    decEq x y = decEqRet watToFish fishToWat fishWatFish x y