निम: कैसे शून्य साबित करने के लिए?

Question

मेरे लिए, निम की सबसे दिलचस्प विशेषताओं में से एक not nil एनोटेशन है, क्योंकि यह मूल रूप से संकलक की मदद से एनपीई/एक्सेस उल्लंघन बग के सभी प्रकारों को पूरी तरह से रद्द करने की अनुमति देता है। हालांकि, मुझे अभ्यास में इसका उपयोग करने में परेशानी है। के सबसे बुनियादी उपयोग के मामलों में से एक पर ध्यान दें:

type 
    SafeSeq[T] = seq[T] not nil 

यहाँ एक तत्काल ख़तरा है कि यहां तक ​​कि instantiating इस तरह के एक SafeSeq इतना आसान नहीं है। प्रयास

let s: SafeSeq[int] = newSeq[int](100) 

त्रुटि cannot prove 'newSeq(100)' is not nil, जो आश्चर्य की बात है, क्योंकि एक उम्मीद कर सकते हैं कि एक newSeq बस नहीं के बराबर नहीं है के साथ विफल रहता है।

proc newSafeSeq*[T](size: int): SafeSeq[T] = 
    # I guess only @[] expressions are provably not nil 
    result = @[] 
    result.setlen(size) 

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

let a: SafeSeq[int] = @[1,2,3] 
let b: SafeSeq[string] = a.mapIt(string, $it) 

सामान्य समस्या यह है कि जैसे ही एक वापसी प्रकार एक साधारण seq हो जाता है संकलक not nil संपत्ति के बारे में भूल करने लगता है और अब यह साबित कर सकते हैं लगता है।

proc proveNotNil*[T](a: seq[T]): SafeSeq[T] = 
    if a != nil: 
    result = a # surprise, still error "cannot prove 'a' is not nil" 
    else: 
    raise newException(ValueError, "can't convert") 

# which should allow this: 
let a: SafeSeq[int] = @[1,2,3] 
let b: SafeSeq[string] = a.mapIt(string, $it).proveNotNil 

हालांकि, संकलक भी यहाँ not nil साबित करने के लिए विफल रहता है:

मेरा विचार अब एक छोटा सा (यकीनन बदसूरत) सहायक विधि मुझे वास्तव में not nil साबित करने के लिए अनुमति देता है कि लागू करने के लिए किया गया था। मेरे प्रश्न हैं:

• मैं संकलक ऐसे मामलों में not nil का निष्कर्ष निकालते कैसे मदद चाहिए?

• इस सुविधा के साथ दीर्घकालिक लक्ष्य क्या है, यानी not nil अधिक शक्तिशाली बनाने की योजना है? मैनुअल proveNotNil के साथ समस्या यह है कि यह संभावित रूप से असुरक्षित है और इस विचार के विरुद्ध कि संकलक इसे साबित करने का ख्याल रखता है। हालांकि, अगर proveNotNil केवल दुर्लभ मामलों में आवश्यक होगा, तो इससे ज्यादा नुकसान नहीं होगा।

नोट: मुझे पता है कि seq प्रयास nil नास्तिक, होना करने के लिए जैसे कि, सब कुछ काम करता है ठीक भी nil मामले में। हालांकि, यह केवल के लिए निम के भीतर लागू होता है। जब सी कोड इंटरफ़ेस, शून्य-छुपा-सिद्धांत, कीड़े के लिए एक खतरनाक स्रोत बन जाता है क्योंकि एक nil अनुक्रम निम तरफ केवल हानिरहित है ...

Answer 1

उपयोग isNil शून्य के लिए जाँच करने जादू:

type SafeSeq[T] = seq[T] not nil 
proc proveNotNil[T](s: seq[T]): SafeSeq[T] = 
    if s.isNil: # Here is the magic! 
    assert(false) 
    else: 
    result = s 
let s = proveNotNil newSeq[int]()