2020-09-29, Теория категорий для программистов
    https://habr.com/ru/companies/piter/articles/521120/

2020-03-02, Монады как паттерн переиспользования кода
    https://habr.com/ru/post/490112/

2014-12-15, Теория категорий для программистов: предисловие
    https://habr.com/ru/articles/245797/

2010-06-06, [Ищу] Учебник по теории категорий
    https://dxdy.ru/topic37813.html

2008-08-22, теория категорий (для чего используется?)
    https://dxdy.ru/post140359.html

---

книга - Сандерс МакЛейн «Теория категорий для математиков»
    1971-1978, Saunders Mac Lane, Categories for the working mathematician

Бартош Милевский (тоже грозился написать книгу, постит по главе в своем блоге, надо проверить - написал или нет)

Glynn Winskell. Event Structures

Хэнк Барендрегт. Лямбда-Исчисление, глава о категорных моделях.
    1985, Барендрегт, Ламбда-исчисление. Его синтаксис и семантика

---

«После большого количества подобных текстов, так и не понял, зачем теоркат программисту. Обещают революцию, а на деле оказывается, что есть пара паттернов типа монад или стрелок, их можно использовать, конец. ... Пока я в подобных статьях видел только ввод в терминологию (вот видишь этот паттерн, он называется монада в категории, где объектами являются типы данных языка, а стрелками — функции), и все. ... Я не нашел в книге Маклейна вообще ничего, что было бы применимо в программировании. Никакой теоремы или приема. Ну диаграммы. Ну коммутативны. Ну и что. Поэтому и спрашиваю.»

«Кто-то исследовал теор. кат. и удачно применил идеи оттуда в программировании. Молодец. Но программирование идеи черпает и из живой природы и из физики и много откуда ещё. Почему в этом ряду выделяют именно теорию категорий мне не понятно. ... вижу только бесконечные попытки натянуть сову на глобус, теорию категорий на все программирование. ... Я не вижу каким образом теория категорий является таким же теоретической основой для программирования, хотя подается она именно так. Я такую основу давно ищу и буду рад если вы меня переубедите.»

«Зачем кому-то захотелось размышлять о программах в таком стиле я не знаю. Каких-то нетривиальных теорем из всего этого не вытекает.»

Главные вопросы, на который надо найти ответ: "зачем изучать теорию категорий программистам", "каким программистом изучать её надо, а каким не надо", "в каком объёме надо знать теорию категорий".

«теория категорий вместо того, чтобы иметь дело с деталями, оперирует структурой.
Она оперирует такими понятиями, которые делают программы компонуемыми.»

«композиция — суть программирования»

«Функциональное программирование ... делает параллелизм компонуемым»
«производит неверное впечатление, что ФП (Функциональное программирование) — это про ТК (теорию категорий), про математику и прочий HOTT.»
«важнейшая польза этих паттернов — легкая и безопасная композиция concurrency и parallelism примитивов. »

«Это послужило основой для создания функциональных языков, в которых возможно написание программ с одновременной верификацией их кода.»

«Композиция функторов — функтор. Композиция естественных преобразований — естественное преобразование. ... Глубже — катаморфизм как обобщение рекурсии. Линзы придумать без теорката имхо анриал.»

«Побочные эффекты не масштабируемы, а императивное программирование полностью построено на побочных эффектах.»

«Идея объединения данных с мьютексом, который их защищает, хороша, но, к сожалению, блокировки не компонуемы, и сокрытие блокировок делает дедлоки более вероятными и менее отлаживаемыми.»

«В программировании обычно приходится работать с подкатегорией функторов, так называемыми эндофункторами, которые помогают отобразить категорию саму на себя. Поэтому просто оговорюсь, что, говоря о функторах, я имею в виду эндофункторы.»
«монада – это просто моноид в категории эндофункторов»

«[теория] типов должна быть понятна любому»

«в теории категорий мы стремимся отойти от множеств»

«объекты – это абстракции, и могут представлять что угодно. Следовательно, мы имеем полное право сказать, что наши объекты – это множества, и далее рассматривать наши программы на Scala как категории, где типы – это объекты, а функции – это морфизмы.»

«монада – это просто некий тип-обертка, поддерживающий некоторый метод для принятия функции и отображения ее самой на себя.»
«Структура Option сохраняется, но теперь в ней содержится либо Sand, либо None, вместо Rock либо None.»
«морфизм в центре – это функтор, представляющий отображение с T на Option[T].»
«Монада — это нечто единое, потому что основное свойство монады — это умение сливаться воедино. Когда мы можем Конструкцию из Конструкций снова превратить в Конструкцию. Список из Списков просто в Список. Или Операцию с Диском из Операций с Диском снова в единую Операцию с Диском. Это основная механика монады, и она прям почти по словарю философских терминов.»
«Монада — худшее название ever. Потому что:
а) Часть людей не знает что такое монада на бытовом смысле.
б) Часть знает — и пытается понять каким образом психологические монада и диада используются в программировании. (плохая омонимия).»
«мой человеческий мозг для эффективного отличения моноида от монады требует бытового ощущения от них. Я с лёгкостью могу почувствовать разницу между переменной и константой (у них в названии прям всё сказано), между файловым деревом и графом зависимостей (который может быть ненаправленным и циклическим и всё портить). А вот между моноидом и монадой — не могу.»
«Моноид — это «однообразие». Моно — это «одно», а оид — это «подобный». Гуманоид.»
«Монада потому что её коммутативным диаграммы очень похожи на диаграммы моноида, самым важным свойством моноида является наличие единицы ...
У меня есть (?) задача, и для решения этой задачи хорошо подходит "монада", потому что главное потребительское свойство монады — это (?), что очевидно из её названия. ... Чуете где проблема? Вторая сложная задача в IT, кстати.»
«Помогает практика использования монад и какая-никакая, а программистская интуиция, нарабатываемая примерами. ... проблемы с изучением Хаскеля — в неверных подходах к обучению.»

«Осталось объяснить пользу от использования кучи терминологии в разговорах о типах-обёртках»
«новые языки программирования успешно избегают использования монад, предоставляя все преимущества от полезных идей, проистекающих от монад. Тот же раст — весь полон монад (Result, Some, Either, etc), но слово "монада" нигде не встречается. Вместо этого дают приятный сахар (с глубокими архитектурными последствиями) и массу гарантий качества.»
«все хотят монад, но на самом деле всем нужна do-нотация... Это такой языковой способ избавляться от "лесенки" колбеков и писать код на одном уровне. Нечто вроде сопрограмм с их оператором await, но с возможностью многократного возобновления с одной и той же точки.»

«у нас есть такая замечательная идея как "труба". Она позволяет объединить выход одного с входом другого. Главное свойство трубы — она транспортирует данные из точки в точку и не проливает (не теряет), хотя может чуть-чуть в себе держать и доносить с задержкой.»

«Я могу использовать "отображения" у себя в программе? Во-первых, вы можете написать функцию (отображение значения в значение). Во-вторых, вы можете написать обобщенный тип (отображение типа в тип). В принципе, отображениям из типа в значение и из значения в тип также может найтись место. Обобщённый класс с ассоциированной константой и зависимый тип (или просто дженерик, параметризованный константой), соответственно,»

«Теория групп и теория полугрупп, в основном, возникли из необходимости описывать преобразование пространства. Если мы будем смотреть на преобразования какого-то пространства самого в себя, то получим как раз однообразие преобразований (все преобразования похожи, однотипны), где бинарная операция — это композиция преобразований.»

«В этом месте прибегают конструктивисты и задают вопрос: что означает «берём»?»

«Множества и рекурсия — понятия плохо совместимые. А в категорных топологических терминах получилось. Конечно, хорошая мысля приходит опосля, и семантика потом была построена и в терминах теории множеств, но изначальная конструкция была категорной.»

«Смысл требования в том, что оно требуется. Это называется аксиоматической подход.»
«Самый известный пример — это ошибки в CompCert (верифицированный компилятор С). В нём регулярно встречаются ошибки, связанные с неверным аксиоматическим описанием процессоров и памяти. ... Технология трудоёмкая, от ошибок не избавляет, сами ошибки становятся трудноуловимыми (потому что, поди разберись, какая из 1000 аксиом сформулирована неверно)»

---

Ранее (по теме?): Массив

Отредактировано Лис (2024-08-13 09:23:59)