а всего-то абстрактные кружочки без структуры, и стрелочки между ними )))
Например "универсальное свойство" -- элементарщина для программистов:
есть спека "из таблицы users вынимаем поле id и прибавляем 1, и поле name делаем trim, и записываем соответственно в Id и Name класса User", сам User активно у нас используется в домене как базовая модель. Также спека, как десериализуем из json в Id и Name в User, и т.п.
Так вот, универсальное свойство просто про то, что корректно конвертнуть в плане маппинга полей Id и Name допускается строго одним способом. А если например тимлид скажет: "да пофиг, хочешь для name в Name делай trim, а хочешь нет", это будут два разных способа, и универсального свойства для User уже не будет (и на самом деле из-за этого в проекте могут возникнуть большие проблемы, подумайте почему).
В некотором смысле User -- это идеальный чистый шаблон в нашей бизнес-логике, никак не связанной с внешним миром (как и например Tuple, Task, IEnumerable из стандартной либы), и для его формирования из любого другого типа существует ровно одна уникальная функция. При том, что сигнатура её ничего не говорит о внутреннем устройстве этих типов (но мы можем делать из неё далеко идущие выводы:). И если этой же функцией сформировать Person, то мы можем считать, что Person и User изоморфны.
(Сермяга на самом деле в другом: мы определяем наш идеальный тип только через уникальные функции/стрелки, его формирующие из других типов; а в целом и из него тоже исходят уникальные функции в любые другие типы).
Но когда типы посложнее
Task<Task<int>> nestedTask = ...;как же трудно пояснить, как это делать (научить как это делать) на C#/Java, чтобы компилятор - система типов - сам отсекал любые способы, отличные от единственно верной стрелки.
c#
Func<Task<Task<int>>, Task<int>> flatten = async outerTask =>
Task<int> innerTask = await outerTask; int result = await innerTask; return result; };
Тут помогает await (универсальное свойство монады), но я могу написать свои ужасающие реализации вроде
Func<Task<Task<int>>, Task<int>> bad = async t => (await t).Result;которые компилируются, но нарушают асинхронность, теряют данные и исключения, приводят к дедлокам...
...И тут на помощь приходят те самые "Theorems for free".
Сколько таких функций вы можете написать, чтобы компилятор вас не забанил?
Func<T, U, T> f = (t, u) => ???;Ровно одну :)
Фактически, изоморфизм Карри-Ховарда говорит ровно то, что строгая типизация с дженериками/тотальный параметрический полиморфизм, и теория категорий -- это буквально одна и та же наука, просто записанная разными буковками.
Влюбился прям в теорию категорий ❤️ следом за HoTT ❤️