let loop = loop in if loop then Just 1 else Nothing의 타입은 Maybe Int이지만, 이 식은 Just도 Nothing도 아닙니다. 타입이 있다고 해서 이 식이 값에 도달하는 것은 아닙니다. 평가기가 단계 예산을 다 쓰고 멈추는 순간 이 차이가 중요해집니다. 예산이 떨어지면 래퍼는 NotFound라고 해야 합니까? 저는 아니라고 보고, Unfinished를 돌려주겠습니다. NotFound는 끝까지 진행해서 없음을 보인 탐색의 몫입니다. 예산이 바닥났다는 사실은 더 진행하면 해를 찾을지에 대해 아무것도 증명하지 않습니다.
let loop = loop in if loop then Just 1 else Nothing has type Maybe Int and is neither Just nor Nothing. The type doesn't make it total. That matters once an evaluator halts after a step budget. When the budget runs out, should the wrapper say NotFound? I'd say no, and return Unfinished. NotFound belongs to a search that completed and showed absence. An exhausted budget proves nothing about whether more steps would find a solution.