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

[rockclimber]

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

(Лирическое вступление, которое можно не читать)

Вкратце перечислю, с чего именно началось (в хронологическом порядке).
1. Несколько лет назад на одном программерском форуме обсуждалась относительно простая учебная задача (не уверен, что правильно помню, что за задача, кажется, нужно было написать простенький парсер арифметических операций). Я написал свой вариант, который состоял из примерно 50 - 150 строчек (точнее не помню). Каково же было мое удивление, когда некто выложил решение той же задачи на Haskell, и оно состояло из 4 (четырех) строк! Сказать, что я был в шоке, это ничего не сказать.
2. Пару лет назад видел комментарий на Хабре о том, что теория категорий - это штука, полезная для программистов, любому может пригодиться (это все, что я помню о том комментарии, контекста не помню).
3. Недавно прочитал на том же Хабре статью про Haskell: Говорят, Haskell — язык для гениев и академиков. Правда? Там тоже теория категорий упоминается.

Поискал по запросу "теория категорий в программировании". Из более-менее приличного на русском нашел цикл статей на том же Хабре: https://habr.com/ru/post/246009/ (это вторая статья из цикла, всего их пять, чтение займет примерно полчаса, в первой - сплошная вода да философия, можно пропустить). В статье рассказывается, какие вещи из теории категорий реализованы в Haskell, с пояснениями, как то же самое выглядело бы на C++. Проблема в том, что я не знаю ни теорию категорий, ни Haskell, так что не всегда понятно, где заканчивается одно и начинается другое. И С++ я тоже не знаю, поэтому что вообще происходит, тоже не всегда понятно (проще сказать, что понятно: полностью понятен только пример с факториалом, пожалуй).
Посмотрел видео https://www.youtube.com/watch?v=JMP6gI5mLHc (1 час, на английском, некто Эрик Мейер рассказывает java-программистам о том, какие из новых концепций в java пришли из теории категорий). Под конец, правда, тоже стало непонятно, потому что теорию категорий я все еще не знаю.

Еще я скачал учебник теории категорий, написанный george66. Пара цитат оттуда:

Цитата:

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

Цитата:

Для чтения книги нужно шапочное знакомство с понятиями "группа", "свободная группа" и "гомоморфизм групп". Если читатель их не знает, советую сначала прочитать популярную книжку Александрова "Введение в теорию групп".

Если отсчитывать от уровня человека, полностью освоившего стандартную школьную программу - это единственное требование или понадобится что-то еще? Написано же "доступный мат.логикам", а я определенно не мат. логик.

Хотелось бы понять, как именно теория категорий помогает программированию. Позволяет взглянуть под другим углом на какие-то аспекты этой деятельности? Позволяет лучше понять какие-то концепции или предлагает свои? Есть ли там такие-то подходы, которые можно использовать везде, или нужна "поддержка" со стороны языка/компилятора (для чего и придумали Haskell)? Пока, к сожалению, не могу сформулировать вопрос четче, буду рад любым наводящим вопросам.
Еще хотелось бы порасспрашивать про Haskell, но из каши в голове складывается максимум "расскажите что-нибудь" или "ну и что там в Haskell с теорией категорий?", остальное пока не членораздельно. Надеюсь, в будущем доберусь и до него.

[arseniiv]

rockclimber в сообщении #1376646 писал(а):

Есть ли там такие-то подходы, которые можно использовать везде, или нужна "поддержка" со стороны языка/компилятора (для чего и придумали Haskell)?

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

Я видел ка категорными штуками сокращали количество boilerplate в коде, но что-нибудь конкретное разумно описать не смогу.

[rockclimber]

arseniiv в сообщении #1376682 писал(а):

Я видел ка категорными штуками сокращали количество boilerplate в коде, но что-нибудь конкретное разумно описать не смогу.

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

[Munin]

rockclimber в сообщении #1376646 писал(а):

Из более-менее приличного на русском нашел цикл статей на том же Хабре: https://habr.com/ru/post/246009/

На беглый взгляд, это не очень-то про Haskell. И даже не очень-то про категории.

[warlock66613]

rockclimber в сообщении #1376738 писал(а):

Но непонятно, есть ли тут такие.

Боюсь что даже если такие и есть/были бы, этого совершенно недостаточно. Знания теории категорий и программирования недостаточно, что понять как одно можно связать с другим.

-- 18.02.2019, 01:29 --

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

И даже не очень-то про категории.

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

[rockclimber]

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

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

Нужна просто какая-нибудь коммутативная диаграмма, или диаграмма, иллюстрирующая нечто конкретное, обсуждаемое в статье? "Просто какая-то диаграмма" там была (https://hsto.org/getpro/habr/post_image ... 72e746.jpg) - как я понимаю, исключительно с целью показать, что такое "категория".

[warlock66613]

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

[Munin]

Я применил более сильный критерий: если нет достаточного количества мотивирующих примеров, то это не про категории.

Для меня достаточно мотивацией было:
1. Оказывается, понятия инъекции, сюръекции и биекции можно сформулировать на языке стрелочек в категории множеств, не описывая детально судьбу элементов при отображениях.
2. Во всех алгебраических системах (группы, кольца, поля, векторные пространства) обычно формулируются одинаковые понятия гомоморфизмов, изоморфизмов, факторизаций, и доказываются похожие свойства и теоремы. Категории позволяют вот эту "одинаковость" выразить явно.

-- 18.02.2019 00:48:01 --

В качестве "примера коммутативной диаграммы", имхо, хорошо подходит диаграмма для определения декартова произведения множеств.

[rockclimber]

Ладно, к черту эту статью. А то подумаете еще, что я ее защищаю (и в мыслях не было).

Вернемся к тому, что нужно знать, чтобы начать изучать теорию категорий:

rockclimber в сообщении #1376646 писал(а):

Если отсчитывать от уровня человека, полностью освоившего стандартную школьную программу - это единственное требование или понадобится что-то еще? Написано же "доступный мат.логикам", а я определенно не мат. логик.

Вот эти понятия

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

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

Это из какого раздела? Высшая алгебра? Теория множеств? Нужно ли их знать (и если да, то до какого уровня), чтобы приступить к изучению сабжа?

И к вопросу о практике.
warlock66613, вы вроде бы и программируете много, и теорию категорий изучали (судя по обсуждению в топике про упомянутый учебник). В общих чертах, что скажете: стоит изучать? До какого уровня? Даже если прямой пользы нет, но есть косвенная.

[Munin]

rockclimber в сообщении #1376793 писал(а):

Это из какого раздела? Высшая алгебра?

Да, только она не называется "высшей". Просто алгебра. Например, Кострикин в 3 томах - очень добрый учебник.

rockclimber в сообщении #1376793 писал(а):

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

По-хорошему, такие вопросы надо переадресовать людям уровня george66.

У меня сложилось такое впечатление:
1. Чтобы ощутить ценность и выгоду от категорий и диаграмм, нужно уже иметь некоторый background в математике, знать какие-то примеры и работу с ними "в некатегорном стиле".
2. Background-ы у разных людей разные, и поэтому люди приходят к категориям "с разных сторон", с разными мотивациями, и ищут в них разное. Поэтому довольно часто то, что написано одним человеком, другого не мотивирует, и наоборот. Я встречал мотивации алгебраические, функциональные, геометрические, и ещё какие-то (теормножественные, может быть). Почти все они мне были не близки.

[warlock66613]

rockclimber в сообщении #1376793 писал(а):

В общих чертах, что скажете: стоит изучать?

Я бы сказал, что ситуация примерно как с теорией множеств. Или функциональным анализом. То есть можно изучать, а можно и не изучать. Во всяком случае, это дальше от практики программирования, чем алгебра.

С алгеброй понятно: многие типы вместе со своими операциями образуют некоторую алгебраическую структуру. Знание типовых структур (моноиды, группы и т. д.) может подсказать способ организации программы, может помочь увидеть нарушения каких-то свойств, которые должны выполняться. Но в общем это уже на пределе практической применимости. А теория категорий ещё абстрактнее. Но потенциально (условная) польза может быть. Так, теория категорий позволяет понять разницу между сюрьективным отображением и эпиморфизмом. А именно, то, что последнее шире. Так что, если я когда-нибудь замечу в своей программе эпиморфизм, не являющийся сюръекцией, я, наверное, смогу сказать "вот, вот зачем нужна теория категорий!"

Есть какая-то витающая в интернетах мысль, что теория категорий имеет прямо-таки непосредственное отношение к программированию - не спроста же эта серия статей на хабре? Но пока для меня это выглядит как миф.

-- 18.02.2019, 10:02 --

Ещё (почти) пример "применения". Типы данных в Haskell образуют категорию $\operatorname{Hask}$, где морфизмами являются функции. На интуитивном уровне эта категория похожа на категорию множеств, и именно так она воспринимается при программировании. Но строго говоря это не категория множеств, и, наверное, теория категорий может cказать каково отношение между этими категориями, благодаря чему мы можем успешно считать типы Haskell множествами, а функции - функциями между множествами.

[alex55555]

rockclimber в сообщении #1376646 писал(а):

Еще хотелось бы порасспрашивать про Haskell, но из каши в голове складывается максимум "расскажите что-нибудь" или "ну и что там в Haskell с теорией категорий?"

В общем оно подавляющему большинству программистов не надо.

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

В целом, если совсем коротко, то скажем так - вот есть теория множеств, которая в простом виде знакома каждому программисту (два круга и их пересечение иллюстрируют операции объединения, пересечения, симметрической разности, просто разности), так вот эта теория программистами (и вроде как и многими математиками) используется лишь как язык для выражения своих мыслей "попроще". Точно так же и теория категорий используется для упрощения подачи каких-то мыслей. Там нет каких-то широко используемых алгоритмов. Если математика даёт нам синусы с косинусами, из которых мы строим космические ракеты, то теории категорий и множеств синусов не дают (ну разве в некоторых узких областях математики), но дают язык для изложения неких общих для многих теорий свойств. И вот этот язык был в своё время применён для изложения подхода функционального программирования к ситуации с "нечистым" программированием, то есть когда появляются сторонние эффекты и функцию функционального языка нельзя рассматривать как математическую абстракцию, никак на окружающий мир не влияющую. Для вывода таких эффектов "в сторону" придумали использовать "ленивые вычисления", то есть запись шагов без их исполнения до того момента, пока не появится возможность выполнить их "чисто", то есть без сторонних эффектов. Ну а на языке теории категорий это всё выразили в виде монад, которые дали своё название для внутренних структур Хаскеля. При этом само по себе решение в виде монад далеко не единственное, и даже с начала в Хаскеле были другие решения, но с какого-то момента авторы прониклись категорным подходом и ввели в язык монады для "отвода нечистот".

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

Но вы, если реально интересно, займитесь. Предупреждаю - это долго. Но если интересно, то интерес обязывает.

[Aritaborian]

alex55555 в сообщении #1376899 писал(а):

Предупреждаю - это долго.

alex55555 в сообщении #1376899 писал(а):

И на выходе вы получите, скажем так, не очень много.

Пессимистичненько. Делаю резюме: «Программисты, забейте, для работы это вам нафиг не нужно».

[Munin]

alex55555 в сообщении #1376899 писал(а):

Там нет каких-то широко используемых алгоритмов.

Обращение стрелочек? Arrow chasing?

alex55555 в сообщении #1376899 писал(а):

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

Это как-то не очень стыкуется с изложением в других местах.

-- 18.02.2019 16:24:38 --

Aritaborian в сообщении #1376901 писал(а):

Пессимистичненько. Делаю резюме: «Программисты, забейте, для работы это вам нафиг не нужно».

Дык примерно так и есть. Для работы даже Haskell не нужен: востребованы C#, Java, Swift, JS, Python.

[arseniiv]

alex55555 в сообщении #1376899 писал(а):

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

Ну это уже никуда не годится. Вычисление с эффектами не может быть произведено без эффектов, стратегия вычисления тут никак не влияет. Ленивость ввели в язык не потому.