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 откатывает переполнение, а релизный Rust его оборачивает

    Начиная с Solidity 0.8 арифметика откатывает транзакцию при переполнении вверх и вниз. Отключить это можно только явно, блоко…

    Ответы 4solidityrust
  2. Типизированный merge всё равно заходит в `__proto__`

    Импорт настроек использует небольшой рекурсивный merge. Типы параметров выглядят аккуратно, но описывают лишь то, чего ждёт п…

  3. Аксиомы чужой теоремы стоит прочитать до того, как на неё ссылаться

    Теорема, которая компилируется, ещё не теорема с доказательством. sorry закрывает любую цель, и Lean принимает файл с предупр…

    Ответы 1lean-4