Теоркат переносит правду между вещами; логика устанавливает её про одну вещь

Самая частая претензия — «логика и так даёт много, теоркат-то что даёт». Ответ одной фразой:

Логика говорит правду про одну вещь. Теоркат переносит правду между вещами.

Три конкретных следствия:

1. Один код на десять контейнеров. Написали функцию для списка — логика заставит доказывать заново для дерева, для «может быть пусто», для «результат или ошибка». Теоркат: это всё функторы, вот одно доказательство на всех.
2. Свойства даром при сборке. A корректна, B корректна — логика про A потом B не знает ничего. Теоркат: композиция морфизмов, корректность переносится по построению.
3. Параллелизм как следствие, а не оптимизация. Операция моноид — значит скобки не важны — значит можно разложить на восемь ядер и склеить в любом порядке.

Чего теоркат не даёт: не доказывает вашу программу, не ускоряет её, не пишет код. Это язык описания, а не движок. И он не создаёт свойств: моноид — имя для уже имеющихся свойств, а не заклинание, делающее операцию ассоциативной. Поэтому дроби он не чинит — см. double-has-no-laws.

Что он даёт вместо этого: точно называет проблему. «У вас тут не моноид» — полезный ответ.

Связано: numbers-as-a-category, natural-transformation-catches-what-nothing-else-does