openlang

탐색 예산이 바닥나면 NotFound를 돌려줘야 할까?

let loop = loop in if loop then Just 1 else Nothing의 타입은 Maybe Int이지만, 이 식은 Just도 Nothing도 아닙니다. 타입이 있다고 해서 이 식이 값에 도달하는 것은 아닙니다. 평가기가 단계 예산을 다 쓰고 멈추는 순간 이 차이가 중요해집니다. 예산이 떨어지면 래퍼는 NotFound라고 해야 합니까? 저는 아니라고 보고, Unfinished를 돌려주겠습니다. NotFound는 끝까지 진행해서 없음을 보인 탐색의 몫입니다. 예산이 바닥났다는 사실은 더 진행하면 해를 찾을지에 대해 아무것도 증명하지 않습니다.

영어에서 번역원문 보기

이어지는 대화 1

서로의 근거를 따라
  1. 고유 링크

    Go로 같은 걸 해 봤어. Unfinished를 센티널로 만들고 %w와 단계 수로 감쌌어.

    var ErrBudget = errors.New("step budget exhausted")
    
    err := fmt.Errorf("after %d steps: %w", n, ErrBudget)
    fmt.Println(errors.Is(err, ErrBudget)) // true
    fmt.Println(err == ErrBudget)          // false

    errors.Is는 맞았어. 옛 호출부 하나가 아직 ==로 비교해서, 예산이 바닥난 탐색을 전부 다른 실패로 처리하고 있었어. 그건 고침. 못 찾은 경우는 그대로 nil 에러에 빈 결과.

    영어에서 번역원문 보기

같은 질문의 다른 갈래

  1. 오버플로 기본값, Solidity의 revert와 Rust 릴리스 빌드의 감싸기

    Solidity 0.8부터 산술 연산은 오버플로와 언더플로에서 revert합니다. 끄려면 unchecked { ... } 블록으로 직접 밝혀야 합니다. Rust는 반대입니다. 디버그 빌드는 panic이 나지만 --releas…

  2. 타입을 붙인 병합 함수가 `__proto__`까지 따라가는 문제

    설정 가져오기 기능이 작은 재귀 병합 함수를 써요. 매개변수 타입은 꼼꼼해 보이지만 프로그램이 기대하는 걸 적어 둔 것일 뿐이에요. 루프는 파싱된 파일에 실제로 있는 키를 그대로 돌아요. JSON.parse는 __proto_…

  3. 의존성의 정리를 인용하기 전에 공리부터 본다

    컴파일되는 정리가 곧 증명된 정리라는 보장은 없다. sorry는 어떤 목표든 닫고, Lean은 경고 하나와 함께 파일을 받아들인다. 다른 곳에서 빌드된 의존성이라면 그 경고는 눈앞에 없다. 확인 수단은 #print axiom…

    답글 1lean-4