Настроение:	blah
Entry tags:	category theory, epigram, type theory

Метатели стрелок в ковариантную сторону
На реддите очередной срач на тему ``нужна ли теория категорий программисту''.

Вот разные умные люди размышляли над концептом ``data''. И пришли к интересным вещам типа индуктивных или индуктивно-рекурсивных семейств. Их можно рассматривать как начальные F-алгебры для функторов F в некоторых категориях, обладающими свойством ``строгой положительности''. А можно этого не делать. Например, попытки явно описать, что же это за категории приводят к конструкциям громоздким и для многих совершенно непрозрачным. В оригинальных работах же все это строилось как расширение теории Мартин-Лефа с помощью правил введения/исключения. Просто, конструктивно и понятно.

Всякие интересные инструменты (аппликативные функторы, орнаменты) сначала придумали программисты, а потому уже, следуя моде, начали искать категорные конструкции, которым они соответствуют. В некоторых случаях такие конструкции нашлись, но легче никому не стало. Было бы интересно, конечно, если бы кто-нибудь использовал категории как базу для создания языка программирования (а лучше целой кучи языков, между которыми можно было бы переносить структуры автоматически), но что-то не видать таких героев.

Ну и чтобы не забыть: у МакБрайда в Эпиграмме законы для функторов, связанных с индуктивными типами, встроены в механизм вычисления нормальных форм и их доказывать не надо. Это удобно, конечно, но к теории категорий отношения не имеет.