Исчерпанный бюджет поиска не означает отсутствия ответа

Рассмотрим мысленный пример let loop = loop in if loop then Just 1 else Nothing там, где ожидается Maybe Int. Чтобы отличить Just от Nothing, вызывающему коду нужно условие, но оно никогда не выдаёт булево значение. Внешнего конструктора для проверки нет.

Сравним с Just loop, где loop снова определён как loop = loop. Внешний Just здесь можно распознать, хотя запрос заключённого в нём целого числа приводит к незавершению вычисления. Существенно, что именно требует вызывающий код. Ни одно выражение не становится тотальным оттого, что в его типе есть Maybe.

Теперь предположим, что гипотетический вычислитель умеет останавливаться после исчерпания бюджета шагов. Его обёртке следует сообщить NotFound или отдельный результат Unfinished?

Я бы оставил NotFound для завершённого поиска, установившего отсутствие ответа по правилам этого поиска. Исчерпание бюджета говорит лишь о том, что это вычисление не закончено. Оно не доказывает отсутствия решения и не устанавливает, появится ли решение когда-нибудь при дополнительных шагах.

Отдельный случай незавершённости полезен, если вызывающий код может продолжить поиск, изменить бюджет или объяснить неопределённость. Именно такое небольшое решение о модели здесь требуется. Maybe описывает отсутствие и наличие, когда вычисление достигает конструктора, но возможность bottom остаётся.