А мне это надо??

Легендарная "Теория категорий для программистов" Милевски,
русский перевод PDF

Классный разбор теорката от Сергей Свиридов, активно пишется, на скале

Лет 5+ назад я сделал трек по вычислительным моделям на Julia - именно на этом языке по наводке мудрейших, и как прозорливо это оказалось: по сути только для этого языка реализована полноценная вычислительная теория категорий - AlgebraicJulia, причём активно пилится.

В принципе в Agda или Lean теоркат как-то формализован, т.е. там работают доказательства автоматически, но писать на них оочень нудно.

Хаскель наоборот более практичен, собственно основы теорката в нём база. Но из-за того что они глубоко встроены в язык, он скорее провоцирует думать базовыми абстракциями теории категорий,

а вот в AlgebraicJulia категорные структуры (в частности моноидальные и дуальные, чего нет в хаске) явно вычислимые. Да, пока нету профункторов, Кан-экстеншенов, но это временно.

Если вы жавишник, можете взять arrow для котлина,

шарписты юзают F# с либами, он конечно в этом плане послабее даже скалы, и к сожалению потенциал его сильно ограничен просто самой системой типов NET, теоркату с ней приходится постоянно сражаться :)