Теория категорий, Haskell и программирование вообще

[warlock66613]

То есть можно сформулировать следующую гипотезу. Программисту действительно полезно прочитать эту книгу, а также, возможно, ряд других книг книг, в названии которых упоминается "теория категорий". Из этого делается ошибочный вывод, что программисту полезно иметь хотя бы самое поверхностное представление о теории категорий.

[vpb]

По моему (не маленькому) опыту, теория категорий математиками используется так: $10 \%$ --- по делу, а $90 \%$ --- для произведения впечатления на девушек и других неосведомленных людей (цифры, конечно, весьма условные). Или для надувания щек перед самим собой. В программировании, вероятно, это соотношение еще более драматическое.

[Legioner93]

warlock66613 в сообщении #1378054 писал(а):

Тут на Хабре проскочила интересная ссылка на книгу Category Theory for Programmers
. Судя по оглавлению, эта книга не является учебником теории категорий, и вот именно её программисту почитать не помешало бы - по крайней мере такому, кто уже начал осваивать хотя бы один функциональный язык (хотя бы тот же F#).

warlock66613 в сообщении #1378062 писал(а):

То есть можно сформулировать следующую гипотезу. Программисту действительно полезно прочитать эту книгу, а также, возможно, ряд других книг книг, в названии которых упоминается "теория категорий". Из этого делается ошибочный вывод, что программисту полезно иметь хотя бы самое поверхностное представление о теории категорий.

Тогда отношение теории категорий ($\text{ТК}$) к "теории категорий для программистов" (приложение ТК, то есть $\text{П(ТК)}$) немного напоминает отношение Теории Упругости ($\text{ТУ}$) к сопромату ($\text{П(ТУ)}$). Сопромат тут неоднократно обсуждался

Вот вам, дети, монады -- с помощью них мы будем рассчитывать арки читать файлики.
Вот вам F-Алгебры, с помощью них мы будем суммировать дерево.
Вот вам коммутативные диаграмы, с помощью них мы будем иллюстрировать свои мысли и сойдём за умных

$$ \xymatrix{ \text{П(ТК)} \ar[rr]^{\text{П(?)}} & & \text{П(ТУ)} \\ \\ \text{ТК} \ar[rr]^{\text{?}} \ar[uu] & & \text{ТУ} \ar[uu] } $$

[Munin]

vpb в сообщении #1378070 писал(а):

По моему (не маленькому) опыту, теория категорий математиками используется так: $10 \%$ --- по делу, а $90 \%$ --- для произведения впечатления на девушек и других неосведомленных людей (цифры, конечно, весьма условные). Или для надувания щек перед самим собой.

Я подозреваю, в начале 20 века примерно то же можно было сказать про функциональный анализ, или про бескоординатную дифференциальную геометрию многомерных многообразий.

[alex55555]

_Ivana в сообщении #1377870 писал(а):

Нормальная и аппликативная стратегии редукции лямбда-термов вводятся чуть ли не с первых страниц любого букваря. Приоритетный левый внешний редекс или левый внутренний редекс, и т.п. Теоремка даже на этот счет есть - что если терм достиг нормальных форм по нормальной и по аппликативной стратегиям, то эти формы совпадают с точностью до альфа-конверсии. В Хаскеле смешанная стратегия колл бай нид - до вик хэд нормал форм, если аргументы конструктора типа не помечены как строгие, о чем уже неоднократно писали выше. Сколько можно писать простыни глупостей ученому соседу?

Было бы интересно понять, в каком месте лямбда исчисления можно найти указание на соответствие понятий "call by need", "call by value" и "call by reference" чему-то из приведенного выше занимательного текста.

-- 24.02.2019, 18:22 --

Munin в сообщении #1378082 писал(а):

Я подозреваю, в начале 20 века примерно то же можно было сказать про функциональный анализ, или про бескоординатную дифференциальную геометрию многомерных многообразий.

Я читал статьи про использование терминов из теории категорий в применении, например, к экспорту/импорту данных из одной БД в другую. Суть очень короткая - назвали одну базу одной категорией, вторую второй, указали, что экспорт/импорт является функтором, и всё. Далее - весь экспорт/импорт предлагается сделать кому-то другому (но на новом уровне понимания, очевидно).

Некоторое обобщение ряда понятий из разных теорий действительно интересно, но в применении к программированию я ничего более интересного, чем переименование известных задач пока не встречал. Хотя да, я не читал всех статей по теории категорий и даже наверняка некие обобщения могут реально упростить какие-то моменты в программировании, но пока что все ссылки, которые я находил в отношении применимости ТК к программированию вели в лучшем случае к предложениям вроде описанного выше экспорта/импорта. Хотя может я чего-то не понял. Но экспорт/импорт пока что точно не упростился.

[vpb]

Munin в сообщении #1378082 писал(а):

Я подозреваю, в начале 20 века примерно то же можно было сказать про функциональный анализ, или про бескоординатную дифференциальную геометрию многомерных многообразий.

Нет. "Теория" категорий --- это язык, и система весьма общих, почти философских, понятий. Обычно она на нужна; случается, удобна; иногда совершенно необходима. А функан и дифгем с самого начала были трудными содержательными науками.

Впрочем, бывают категории не как средство языка, а конкретные алгебраические системы, типа групп. Где одно в другое плавно перетекает --- не вполне определенно. Еще бывают $n$-категории. Это уже совсем конкретная математика, а не язык.

[warlock66613]

Я почитал упомянутую книгу. Всё-таки она оказалась учебником по теории категорий. То есть изложенное в первой главе ещё претендует на связь с программированием, но начиная со второй примеры на C++ исчезают, а роль примеров на Haskell инвертируется: не теория категорий объясняет суть кода, а код объясняет теорию категорий (а зачем такой код вообще имеет смысл писать, не объясняется). Единственное исключение - пляски вокруг монад (и немного комонад), но и тут неясно, даёт ли это что-то новое для практического применения этих концепций по сравнению с примитивным пониманием. В итоге, роль теории категорий в основном сводится к помощи в поиске названий (если что-то похоже на функтор - назовём это функтором).

[alex55555]

warlock66613 в сообщении #1378324 писал(а):

Я почитал упомянутую книгу. Всё-таки она оказалась учебником по теории категорий.

Вообще я встречал несколько книг с подобными названиями - для программистов, для математиков, для учёных. Но все про теорию категорий. Видимо маркетинг такой - выделять целевую аудиторию и как-то привлекать её, например названиями. Хотя не скажу, что плохо пишут, но просто знаю, что это всё довольно живой бизнес, где автор пусть и не так много, но зарабатывает. Чуть более яркий пример - The Complete Idiot's Guide to Microsoft Access 97. Тоже люди зарабатывают, и даже аудиторию прямо в лицо называют, ведь аудитории действительно нужно по быстрому получить результат, вот им и подсказывают.

warlock66613 в сообщении #1378324 писал(а):

В итоге, роль теории категорий в основном сводится к помощи в поиске названий

Может когда-нибудь за счёт перехода от рисования разного рода блок-схем к написанию неких выражений, как это было в своё время при переходе от чистой геометрии к её алгебраическому варианту, что-то да получится.

[arseniiv]

warlock66613
Ну вот разговоры про codensity monad, например, по-моему, не просто «мы нашли идею совершенно без теорката и потом уже увидели её и там и взяли оттуда имя». Кажется, там какие-то категорные результаты как минимум облегчали понимание (я дотуда ещё не дошёл, так что у меня нет понимания, чтобы облегчать). На эту тему много писал среди прочих Edward Kmett (хотя немудрено, он автор соответствующего пакета).

[warlock66613]

arseniiv, это так, но обсуждаемая ситуация отлична от той, что в этой истории, сразу в двух аспектах: 1) монады уже изобрели, широко применили, и объяснили уже на самом примитивном уровне; 2) я не знаю, сколь это верно в отношении rockclimber, но я - не Edward Kmett, и ТС, скорее всего, тоже.

[arseniiv]

Что-то я значит опять запутался в контексте.

[george66]

Патрышев от монад балдеет, а программирует на Scala. Кстати, он дружок Бартоша Милевского.
https://juan-gandhi.dreamwidth.org/
А так, не знаю, нужна ли программистам теория категорий. Если бы с редукциями лямбда-термов как-нибудь разобраться, чтобы термы представлять разноцветными схемами и строить в каком-нибудь графическом редакторе (а лучше вязать виртуальным крючком). Тогда бы можно было быстро навязать много надёжного и красивого кода.

[arseniiv]

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

[Munin]

george66 в сообщении #1383266 писал(а):

Патрышев от монад балдеет, а программирует на Scala. Кстати, он дружок Бартоша Милевского.

Вот интересная фраза. Мне сразу пришло в голову, что отдельная личность в математике значит многое, а в программной индустрии - почти ничего. Надо привлечь на свою сторону заметную долю проектов - только тогда это хоть как-то прозвучит.

[_Ivana]

george66 в сообщении #1383266 писал(а):

много надёжного и красивого кода

За красивость соглашусь, писал в свое время визуализированные редукторы




А насчет надежности - сомнительно имхо. Только будем тогда писать формально корректные а фактически ошибочные и неэффективные алгоритмы