Nim: Nasıl değil ispatlamak için?

Question

Bana göre, Nim'in en ilginç özelliklerinden biri not nil ek açıklamasıdır, çünkü derleyici yardımı ile temelde NPE/erişim ihlali hatalarının her türünü tamamen devre dışı bırakabilir. Ancak, bunu pratikte kullanmakta zorlanıyorum. en temel kullanım durumları biri düşünelim:

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

burada Hemen bir tuzak bile başlatmasını böyle bir SafeSeq o kadar kolay değil olmasıdır. girişimi

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

biri newSeq sadece sıfır olmadığını tahmin edebileceğiniz çünkü şaşırtıcı hata cannot prove 'newSeq(100)' is not nil, başarısız olur.

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

bir SafeSeq ile bir şeyler yapmaya çalışırken sonraki sorun ortaya çıkar: Bir geçici çözüm böyle bir yardımcı kullanmak gibi görünüyor. Örneğin, bir SafeSeq üzerinden eşlediğinizde sonuç tekrar sıfırlanmamalıdır. Ancak, böyle bir şey de başarısız:

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

genel sorun bir dönüş türü sıradan bir seq olur en kısa sürede derleyici not nil mülkiyet unutmak gibi görünüyor ve artık bunu kanıtlamak olabilir gibi görünüyor.

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 

Ancak derleyici de burada not nil kanıtlamak için başarısız:

Benim fikrim şimdi aslında not nil kanıtlamak için izin veren küçük bir (belki çirkin) yardımcı yöntemi tanıtmak oldu. Sorularım şunlardır:

• nasıl böyle durumlarda not nil çıkarım derleyici yardımcı olmalıdır?

• Bu özellik ile uzun vadeli hedef nedir, yani, not nil çıkarımını daha güçlü yapmanın yolları var mı? Elkitabı proveNotNil ile ilgili problem, potansiyel olarak güvensiz olması ve derleyicinin bunu kanıtlamaya çalıştığı fikrine karşı olmasıdır. Ancak, proveNotNil sadece çok nadir durumlarda gerekli olsaydı, çok fazla zarar vermezdi.

Not: Ben yani herşey hatta nil durumda ince çalışır seq girişimleri agnostik nil olmak olduğunu biliyoruz. Ancak, bu sadece Nim içinde için geçerlidir. C kodu arabirim zaman bir nil dizisi Nim tarafında sadece zararsız olduğu için sıfır gizleme-prensibi ..., hatalar için tehlikeli bir kaynak haline

Answer 1

Kullanım IsNil nil denetlemek için sihirli:

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]()