Числа описываются категорией, но категория не вычисляет

Идея «зачем брать число у процессора, если можно объявить категорию» — не самодеятельность. В теории категорий это называется объект натуральных чисел (natural numbers object, Ловер, 1964): объект N со стрелками «ноль» и «следующий», такими что рекурсия по ним определена однозначно. Категорное определение чисел.

Граница проходит здесь:

Категория описывает структуру и законы. Она не производит вычисление.

Объект натуральных чисел говорит, какие операции есть и каким законам подчиняются. Он не говорит процессору, как складывать. При исполнении вариантов два:

1. строить числа из структуры — тогда 1000 это тысяча вложенных «следующих», и сложение двух тысяч займёт миллионы шагов;
2. реализовать структуру машинными числами и доказать соответствие.

Второе — то, что делают все, и то, что нужно нам. Категория — спецификация, а не реализация. Число от процессора всё равно нужно; категория говорит, правильно ли им пользуются.

Машинка для этого появилась: объявляемое равенство морфизмов и проверка законов — см. category-theory-transports-truth.

Связано: exact-in-which-base, category-theory-transports-truth