Бесконечность становится законной, если убрать вычитание

Проблема бесконечности не в том, что она бесконечна. Проблема в трёх операциях: ∞ − ∞, 0 × ∞, ∞ / ∞ дают «не число».

Отсюда рецепт: убрать операции — законы вернутся.

Конкретно: неотрицательные числа с бесконечностью, отрезок [0, +∞], по сложению образуют коммутативный моноид. Сложение всегда определено, ассоциативно, коммутативно, ноль нейтрален, бесконечность поглощает. NaN недостижим, потому что вычитания в структуре нет.

Это законный полезный тип: стоимости, расстояния, таймауты, ёмкости — всюду, где «бесконечность» значит «недостижимо» или «без предела».

Дополнительная выгода. Тип с обеими границами — подарок ядру: правила про неотрицательность и умножение уже читают отрезок, так что часть функций становится доказуемой просто от смены объявленного типа.

Статус. Работа запущена (ветка work/beskonechnost) с прямым требованием проверить это рассуждение вычислением, а не принять на слово.

Связано: double-has-no-laws, three-number-types, nan-is-reachable