Счётчик типа нат внутри записи написать нельзя, и это меняет устройство программы, а не одну строку

Любая программа, копящая счёт в поле записи (позиция в файле, число обработанных знаков, длина накопленного), упирается в одно и то же:

FLANG_TYPE: поле «закрыто» записи «Счёт»: ожидался нат, получен число

Причина названа в самом языке: нат — это отрезок [0, 2⁵³−1], а сумма двух значений из него до 2⁵⁴−2, то есть за точной сеткой double. Отрезок, вышедший за сетку, перестаёт быть целым (flang/src/types.mjs, отрезок), и нат плюс нат даёт число. Расширение — это и есть проверка переполнения, и она статическая: сторожа в напечатанном коде нет.

Сужением это не чинится, и вот почему. Соблазн — обложить сумму условием:

пусть сумма равно счёт.«закрыто» плюс счёт.«частично» плюс 1
если (сумма не меньше 0) и притом (сумма не больше 4503599627370495)
  то запись «Счёт» с «закрыто» равным сумма и «частично» равным 0
  иначе …

Не работает. Сужение по условию (сузить в types.mjs) переносит границы, но не восстанавливает целость: она берётся из уже расширенного типа (поСравнению(op, предел, целыйЛи(узкий))). Значение стало число — числом и останется, какими границами его ни обкладывай.

Что работает. Сужать надо ОПЕРАНДЫ, до сложения, и только имена: сравнение читает имя с литералом, а не поле и не вызов. Тогда сумма считается заново и в сетку укладывается:

если начало не больше 99999999999999
  то (начало умножить на 10) плюс цифра     // остаётся нат

Второе, что здесь мешает и стоит знать заранее: у результата ВЫЗОВА верх виден только по объявленному типу. Функция возвращает нат для вызывающего — это весь отрезок [0, 2⁵³−1], сколько бы она ни возвращала на самом деле. Поэтому (начало умножить на 10) плюс («Цифра числом» от голова) разваливается даже при суженном начало: второе слагаемое приезжает во всю ширину. Лечится тем же — связать пустьом и сузить: пусть цифра равно «Цифра числом» от голова, затем цифра не больше 9 в условии.

Устройство программы от этого меняется по-настоящему. В журнале упреждающей записи (examples/wal/write-ahead-log.flang) счётчика съеденных знаков нет вовсе — и это не обход запрета, а лучшее решение, к которому запрет подтолкнул. Сколько знаков занято, говорит длина печати восстановленных записей; длина натуральна по построению, и вопрос отпадает. Побочная выгода больше основной: главное утверждение файла стало «печать прочитанного совпадает с прочитанными знаками», а было бы «два счётчика согласны между собой».

Чем подтверждено. Прогоны flang check на четырёх пробных модулях (нат в поле объекта и в поле варианта — принимаются; нат плюс нат в поле — FLANG_TYPE; сужение конъюнкцией после пусть — та же диагностика; сужение операнда — принимается). Ветка work/zhurnal-wal, модуль журнала: 25 функций, все тотальные, сторожей в рантайме 0 мест.

Чем ограничено. Про свёртка это не «мешает», а «невозможно»: тип накопителя свёртки не уточняется вовсе (объявить его негде), поэтому свёртка всегда отдаёт число. Где нужен нат — писать разбор и рекурсию; заодно тотальность несётся структурой, а не мерой, и сторожа не появляется.

Связано: three-number-types, a-record-field-laundered-a-value, left-fold-gives-no-list-induction, rule-one-does-not-read-calls-and-fields