Idiomatic बूलियन समानता उपयोग (सिंगलेट्स)

Question

मैं प्रतीक का उपयोग कर प्रकार स्तर पर टैग की गई वस्तुओं को स्टोर करने के लिए एक डेटा संरचना बनाना चाहता हूं। यह:

data Store e (ss :: [Symbol]) where 
    Nil :: Store e '[] 
    Cons :: e s -> Store e ss -> Store e (s ': ss) 

data HasElem (a :: k) (as :: [k]) where 
    AtHead :: HasElem a (a ': as) 
    InTail :: HasElem a as -> HasElem a (b ': as) 

class HasElemC (a :: k) (as :: [k]) where hasElem :: HasElem a as 
instance HasElemC {OVERLAPPING} a (a ': as) where hasElem = AtHead 
instance HasElemC a as => HasElemC a (b ': as) where hasElem = InTail hasElem 

from :: HasElemC s ss => Store e ss -> e s 
from = from' hasElem 

from' :: HasElem s ss -> Store e ss -> e s 
-- from' _ Nil = undefined 
from' h (Cons element store) = case h of 
    AtHead -> element 
    InTail h' -> from' h' store 

थोड़े से काम करता है, अगर आप इस तथ्य है कि संकलक मुझे आपूर्ति नहीं from' _ Nil परिभाषा के लिए चेतावनी दी है की उपेक्षा (? क्यों ऐसा होता है, वैसे वहाँ यह करने से रोकने के लिए एक रास्ता है?) लेकिन क्या मैं वास्तव में चाहता था शुरुआत में करने के लिए अपने स्वयं के प्रकार-स्तर कोड लिखने के बजाय, मूर्खतापूर्ण फैशन में सिंगलेट्स लाइब्रेरी का उपयोग करना था। कुछ ऐसा:

import Data.Singletons.Prelude.List 

data Store e (ss :: [Symbol]) where 
    Nil :: Store e '[] 
    Cons :: Sing s -> e s -> Store e ss -> Store e (s ': ss) 

from :: Elem s ss ~ True => Store e ss -> e s 
from (Cons evidence element nested) = ??? 

दुख की बात है कि मैं संदर्भ को समान रूप से संदर्भित करने के तरीके को समझ नहीं पाया। मैं सिंगलटन लाइब्रेरी से बिल्डिंग ब्लॉक का उपयोग कैसे कर सकता हूं जो मैं करने की कोशिश कर रहा हूं?

ghc@7.10.3, singletons@2.1

Answer 1

Don't use Booleans! मुझे लगता है कि keeprepeatingmyself इस बिंदु पर: बूलियन निर्भर रूप से टाइप किए गए प्रोग्रामिंग में बेहद सीमित उपयोगिता के हैं और जितनी जल्दी आप आदत को बेहतर तरीके से सीख सकते हैं।

एक Elem s ss ~ True संदर्भ आप का वादा किया है कि s कहीं ss में है, लेकिन यह जहां कहना नहीं है। ss की आपकी सूची से s -value के उत्पादन के दौरान आपको यह कमी में छोड़ देता है। एक बिट आपके उद्देश्यों के लिए पर्याप्त जानकारी नहीं है।

इसकी तुलना अपने मूल HasElem प्रकार की कम्प्यूटेशनल उपयोगिता के साथ करें, जो सूची में तत्व की अनुक्रमणिका देकर प्राकृतिक संख्या की तरह संरचित है। (There (There Here) जैसे S (S Z) के साथ मान के आकार की तुलना करें।) ss की सूची से s का उत्पादन करने के लिए आपको केवल अनुक्रमणिका को कम करने की आवश्यकता है।

कहा कि, आप अभी भी की वसूली जानकारी आप दूर फेंक दिया और Elem x xs ~ True के संदर्भ से एक HasElem x xs मान प्राप्त करने में सक्षम होना चाहिए। यह कठिन है, यद्यपि - आपको Elem x xs का मूल्यांकन करने के लिए आइटम () के लिए सूची खोजनी है, जिसे आपने पहले से ही किया है) और असंभव मामलों को खत्म कर दिया है। आगाडा में कार्य (परिभाषाएं छोड़ी गईं):

recover : {A : Set} 
      (_=?_ : (x : A) -> (y : A) -> Dec (x == y)) 
      (x : A) (xs : List A) -> 
      (elem {{_=?_}} x xs == true) -> 
      Elem x xs 
recover _=?_ x []() 
recover _=?_ x (y :: ys) prf with x =? y 
recover _=?_ x (.x :: ys) prf | yes refl = here 
recover _=?_ x (y :: ys) prf | no p = there (recover _=?_ x ys prf) 

हालांकि यह सब काम अनावश्यक है। बस शुरू करने के लिए जानकारी समृद्ध प्रमाण-अवधि का उपयोग करें।

from' :: HasElem s ss -> Store e ss -> e s 
from' AtHead (Cons element store) = element 
from' (InTail i) (Cons element store) = from' i store 

द्वारा:

---

वैसे, आप बाएं हाथ की ओर अपने Elem मिलान करके अधूरा पैटर्न के बारे में आपको चेतावनी GHC को रोकने के लिए, बल्कि एक case -expression की तुलना में सक्षम होना चाहिए जिस समय आप परिभाषा के दाईं ओर हैं, बाएं तरफ अन्य शर्तों के लिए संभावित रचनाकारों को परिष्कृत करने के लिए पैटर्न-मिलान के लिए बहुत देर हो चुकी है।