Как стать автором
Обновить

Теория категорий для программистов. На пальцах

Время на прочтение 7 мин
Количество просмотров 41K
Всего голосов 24: ↑22 и ↓2 +20
Комментарии 131

Комментарии 131

Расскажите, когда следующая распродажа будет, а то я на недавнюю опоздал — обидно! :)
Таким образом, монада – это просто некий тип-обертка (как в примере с обобщенными типами выше), поддерживающий некоторый метод для принятия функции и отображения ее самой на себя.

Что такое монада объяснили.

Осталось объяснить пользу от использования кучи терминологии в разговорах о типах-обёртках :-D

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


Тут очень хорошо написано, на мой взгляд: монады как паттерн переиспользования кода

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

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

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

Есть реляционная алгебра, которая является теоретической основой БД. Она устанавливает пару важных фактов
— Любые манипуляции с отношениями выражаются через фиксированный набор операций (базис этой алгебры)
— Отношения можно нормализовать и получить полезные свойства.

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

Я не DBA, но мне казалось, что и без знаний реляционной алгебры и всех определений из нее можно пользовался реляционными БД. Можно даже знать и применять нормальные формы на уровне эмпирических правил.

Конечно можно, также как можно пользоваться линейной алгеброй без знания топологии и теории множеств. Но мой комментарий был не про это.
Всё-таки между книгой Лэмпорта и книгой «Как мы верифицировали RTOS» нефиговый такой разрыв, который придётся проходить самому :)
НЛО прилетело и опубликовало эту надпись здесь

С реляционной моделью данных (РМД) всё не так просто. При всём уважении к Кодду, Бойсу, Чемберлину, Дейту, Дарвену и прочим титанам.
Та знаменитая статья Кодда 1969-1970 года "Реляционная модель данных для больших совместно используемых банков данных" — это очень важная работа, в которой он сформулировал основные затруднения в существовавших на тот момент времени подходах, предложено манипулировать данные как отношениями и сформулировано понятие нормализации. Но, честно говоря, статья вызывает больше вопросов, чем ответов. И полноценная реляционная алгебра (РА) не была в ней сформулирована.
Последующие работы упомянутых "титанов" худо-бедно сформулировали РА (ну у того же Дейта в его книге "Введение в системы баз данных"). Но и сформулировано это недостаточно формально, и РА в том виде совсем недостаточно для баз данных. Для баз данных нужно было больше, чем теория и под крылом IBM (что характерно, кажется, все перечисленные в первом абзаце работали в IBM) был сделан SQL (теми же Бойсом и Чемберлином). Но SQL отвратительно ложится на РМД и решительно выходит за рамки РА. Этот диссонанс нашёл отражение в 12 правилах Кодда, ну и у Дейта постоянно в книге это вылезает.
Несмотря на это, СУБД с SQL надо было продавать и политически-маркетингово их стали называть РСУБД. Надо отдать должное — всё-таки SQL из коммерчески используемого всё-таки ближе всего к РМД.


Так что как вывод:


  1. РСУБД (а под этим сейчас понимают SQL-СУБД) не "Р".
  2. Сама РА на самом деле дырявая шо пипец (дырки образовались в попытках натянуть РА на СУБД).
  3. Полезное свойство у нормализации только облегчение обеспечение целостности. Почти всё остальное — инженерные практики конкретных СУБД.

Вот я как раз наоборот, уже лет 10 жду когда изыскания в теоркате и более прикладные в функциональном подходе к программированию придут в область СУБД. Тот, кто это осилит в коммерческом продукте — "заправит топливом" теории обработки данных еще лет на 50.

Вы совершенное правы! Теория категорий используется для доказательства верности написанной программы. И это используется в основном при разработке спецификаций. В современном мире спецификациям уделяют мало внимания, хотя это огромный пласт по повышению качества программ и их стойкости к появлению ошибок…
Чтобы не останавливаться на абстрактном конечном автомате для спецификаций, нужно как минимум в части доказательств загнать спецификацию языка программирования, на котором ведётся разработка, а в идеале ещё и поведение железа. Я затрудняюсь оценить сложность по времени разработчиков, как и то, сколько будет крутиться доказательство, чтобы обыграть огромное количество потенциальных состояний и краевых случаев.
С точки зрения практика так глубоко копать не нужно. Спецификация железа и ЯП как часть системы доказательства полезно, но не критично. Критична простота использования, доступность и понятность. Мне бы хотелось доказывать вещи вроде
— Пользователь не может выполнить действие не представив валидный токен.
— Выполнение действия не приведет к неограниченному росту количества записей в БД.
— Действия А и Б можно выполнять параллельно.
— Действие всегда завершится успешно или с ошибкой за ограниченно время (хе хе :)

Если эти доказательства сломаются на каком-то особенном железе или какой-то особенной БД, не беда. Это компромис который, я уверен, индустрия готова принять ради возможности просто описывать указанные выше кейсы.
Первые два кейса точно можно описать, третий — возможно, но я не знаю как :), четвёртый — описывается завершение до тайм-аута.
НЛО прилетело и опубликовало эту надпись здесь
Третий можно, но формализовывать неприятно.
Это доказывается как отсутствие общих ресурсов на модификацию?
НЛО прилетело и опубликовало эту надпись здесь
Так можно и лок-фри-штуки доказывать
А с локами не интересно. Правда, если мне верификатор подскажет, где именно надо ставить лок…
НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь
А вот и примеры: Соответствие Карри — Ховарда гласит, что наблюдаемая структурная эквивалентность между математическими доказательствами и программами, может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями. Это послужило основой для создания функциональных языков, в которых возможно написание программ с одновременной верификацией их кода. Наиболее известными языками такого рода являются Coq и Agda, созданные для формализации математических доказательств. В частности, именно на языке Coq удалось построить формальное доказательство гипотезы четырёх красок и ряда других трудных математических результатов.
Как вы считаете, почему этот подход не находит применения в массовой индустрии? Мне кажется все это слишком тяжело понять. Те же нормальные формы можно освоить и применять за пару дней. Подозреваю, что Coq и Agda потребуют практически заново выучить программирование.
НЛО прилетело и опубликовало эту надпись здесь
Но и в аэрокосмос, промышленность, RTOS, вендорную сторону телекома, банки оно как-то тоже не проникает.
НЛО прилетело и опубликовало эту надпись здесь
У банков куча сторонних механизмов контроля рисков. Если что-то пойдет не так, то в большинстве случаев потери небольшие или транзакции можно повернуть вспять. Грубо говоря там все проверки в рантайме, в виде различных сверок и сведения баланса.
Потому что индустрии не нужны программы, которые значение выражения 2000 — 1000 вычисляют несколько секунд, и в которых простейшие факты, типа reverse = fold cons нужно доказывать много часов. Кроме того, эти системы не спасают от того, что программист доказал какую-то формально корректную ерунду. Часто встречаются тексты, в которых даются некорректные определения, а потом по ним что-то доказывают. Доказательства будут корректными, но сами определения и следствия из них могут быть бессмыслицей. Самый известный пример — это ошибки в CompCert (верифицированный компилятор С). В нём регулярно встречаются ошибки, связанные с неверным аксиоматическим описанием процессоров и памяти.

Технология трудоёмкая, от ошибок не избавляет, сами ошибки становятся трудноуловимыми (потому что, поди разберись, какая из 1000 аксиом сформулирована неверно), а код, который можно получить из Coq или Agda, громоздкий и очень медленный. Его надо переписывать. А переписывание вносит ошибки.

Кроме того, реально важные вычисления, обычно, работают с тем или иным приближением вещественных чисел, а строить про них доказательства пока ещё нормально не научились. Под каждое доказательство, фактически, изобретается своя аксиоматика поля R.

Работы, конечно, идут, чтобы это положение улучшить. Но пока особых успехов нет. Самое многообещающее — это чуть менее, чем призрачная, возможность вместо натуральных чисел, которые стандартно в таких системах представляются списками единичек, без изменения доказательств, автоматически, использовать числа, представленные списками из единичек и ноликов.

Примерно такая картинка. Поэтому в индустрии более популярны системы верификации, основанные на проверке моделей и на абстрактной интерпретации.

Тем не менее, лично я считаю полезным научиться работать в Coq или Idris. Это помогает потом программировать точнее и выразительнее.
НЛО прилетело и опубликовало эту надпись здесь
Поэтому в индустрии более популярны системы верификации, основанные на проверке моделей и на абстрактной интерпретации.


Это уже упомянутый TLA?

Монада — худшее название ever. Потому что:
а) Часть людей не знает что такое монада на бытовом смысле.
б) Часть знает — и пытается понять каким образом психологические монада и диада используются в программировании. (плохая омонимия).


В сравнении с этим большинство других терминов обладает инутитивными свойствами. fiber и thread начинаются и заканчиваются, могут переплетаться. В pipe с одной стороны вливают, с другой выливают. Семафор либо пропускает, либо блокирует движение. Спинлок крутится пока не разблокируется. Список состоит из элементов, причём порядок важен. Типаж (трейт) описывает характерные черты (персонажей).


В сравнении с этим — что такое монада в бытовом смысле? Что от неё ожидать? Что там "моно"?

Царских путей нет. Монада потому что её коммутативным диаграммы очень похожи на диаграммы моноида.

А почему моноид? Что там "моно"? И почему это "моно" является главным свойством, требующим пристального внимания? Вот почему в синглтоне слово "сингл" в начале я могу объяснить. А в моноиде — нет.

Моноид это полугруппа с единицей. Может поэтому.

То есть самым важным свойством моноида является наличие единицы, так? И когда я вижу в коде упоминание монады, я должен помнить, что там есть единица (в контексте функций — identity). И это самое важное свойство и моноида, и монады, на которое опирается вся модель работы?


Здорово! Каждый раз, когда мне нужна единица (или единичная функция) мне надо использовать монады. А почему я не могу использовать просто 1?

Нет, вы все перепутали. Каждый раз, когда вы используете монаду, вы знаете что там есть единица и можете ей воспользоваться.

Ну, вот, давайте разбираться.


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


Теперь, монады. У меня есть (?) задача, и для решения этой задачи хорошо подходит "монада", потому что главное потребительское свойство монады — это (?), что очевидно из её названия.


Чуете где проблема? Вторая сложная задача в IT, кстати.

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

Нет, я не предлагаю называть монаду "трубой". Я приводил в пример описание более простой абстракции — pipe. Она простая, ясная и не требующая открыться глубокому внутреннему миру идеи.

Монада это


  • множество отображений категории на себя (эндофункторов)
  • с бинарной ассоциативной операцией «умножение»
  • с «единицей»

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

Монада это
Эндофунктор с двумя естественными преобразованиями, удовлетворяющим соответствующим равенствам. А не то что вы написали.

Возможно, я просто перефразировал (как мог) «монада это моноид в категории эндофункторов».

Отображение — это крайне интересная штука, кстати. Я могу использовать "отображения" у себя в программе? Какое главное свойство отображения? Оно берёт значения из одного множества и превращает их в множество других значений, причём это всё в декларативном виде. Как только вы сформулировали правила отображения, все значения отображены, и ими можно оперировать как единым целым.


Так, отлично! У меня есть файл на стопятот терабайт, набитый значениями и мне надо их все их отобразить.


Упс, что вы говорите, IO, память, медленно? Но вы же говорили, что отбражения существуют сразу после их декларации… Но у нас же компьютеры, и там всё не так.


Эх, жаль, нельзя использовать отображения.
А, у нас же монады. А монады — это множество отображений.


… А отображения мы использовать (написать) не можем, потому что см выше.


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

Пока я чувствую шаткость ваших аргументов. Отображение и образ отображения это разные вещи.

Давайте проще. Вот у меня есть отображение ℝ -> ℝ.


Стоп. У меня даже ℝ нет и быть не может, а вы тут про отображения… Основная проблема в том, что математические рассуждения отличаются от алгоритмических. В алгоритмических можно использовать результаты математических рассуждений, а объекты большинства математических рассуждений — нет.


Заметим, большинства. В меньшинстве у конечные группы (mod 256 и т.д.), которые можно просто брать и использовать. Конкретные группы, правда, а не множество всех групп, увы.

Следуя вам получается, что теория алгоритмов это не математика.

Теория алгоритмов — математика. Алгоритмы — искусство, для которого доказаны весьма пренеприятные теоремы, по которым это и останется искусством (математики сдались).

НЛО прилетело и опубликовало эту надпись здесь
Но они были доказаны, как раз с появлением в математике понятия алгоритма и формализации через него доказательств. Алгоритмы портят всё :)
Отображение — это крайне интересная штука, кстати. Я могу использовать "отображения" у себя в программе?

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


Я не вижу причин, которые бы помещали использовать всё выше перечисленное при обработке 100500 терабайт данных.

В принципе, отображениям из типа в значение и из значения в тип также может найтись место.

Обобщённый класс с ассоциированной константой и зависимый тип, соответственно?

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

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

Во кавалерия подтянулись. С аргументом не согласен. Новые теории всегда сталкиваются с необходимостью построения названий. И если они находят параллели в уже существующих теориях это хорошо. Иначе периодически пришлось бы вспоминать что Mappble это Functor. А от необходимости учить определения никто не избавлен.
Map вообще появляется от слабой выразительности языка и наличия экспоненты в категории типов.

НЛО прилетело и опубликовало эту надпись здесь

О, тут говорят вы разбираетесь в этом всем. Меня интересует вопрос — есть ли какие-то нетривиальные теоремы в теории категорий, которые имеют отношение к программированию?


Например Фурье показал, что любой периодический сигнал можно разложить в ряд. И это нетривиальный факт, если просто смотреть на такие сигналы, это не очевидно. Есть абстрактная алгебра и теорему о том, что любую алгебру можно вложить в полугруппу. Это тоже нетривиально, оказывается можно реляционную алгебру отобразить в полугруппу. А затем поизучать что там в этой полугруппе происходит.


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

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

Или, например, денотационная семантика языков программирования, которая строится в категории, так называемых, доменов Скотта-Ершова. Денотационную семантику было особенно трудно строить в контексте теории множеств, потому что, в частности, нужно было уметь интерпретировать равенства вида T = T -> T (для бестипового lambda-исчисления) и прочие рекурсивные определения. Множества и рекурсия — понятия плохо совместимые. А в категорных топологических терминах получилось. Конечно, хорошая мысля приходит опосля, и семантика потом была построена и в терминах теории множеств, но изначальная конструкция была категорной.
А можно ссылки? Я бы почитал.
Glynn Winskell. Event Structures
Хэнк Барендрегт. Лямбда-Исчисление, глава о категорных моделях.

А мне не нравится.


Смотрите, у нас есть простые и консистентные обозначения для всего на свете внутри компьютеров:


00000000  56 56 f8 68 91 5d 67 d1  8d f9 4a 94 92 41 05 6f  |VV.h.]g...J..A.o|
00000010  dc 48 c5 3e e5 e3 f3 da  d1 d1 9d 2f c7 d3 e2 c7  |.H.>......./....|
00000020  21 46 8e 11 56 61 e3 92  bc 86 a9 6c 79 f7 31 b5  |!F..Va.....ly.1.|
00000030  49 66 7a 6a db 9d 75 91  80 69 8d 99 fe d9 57 2e  |Ifzj..u..i....W.|
00000040  fd d4 88 42 03 b6 95 a1  fe 17 07 cd 88 11 54 ec  |...B..........T.|
00000050  fe 3d 1d 12 e0 ee e5 88  e4 b9 e5 fd e3 56 08 e3  |.=...........V..|
00000060  c4 45 de 21 87 47 8e 09  bf 5c 13 40 44 43 c1 b3  |.E.!.G...\.@DC..|
00000070  eb 59 a0 6e cb 1f 6b 3c  bf a6 40 88 fe 48 aa d0  |.Y.n..k<..@..H..|
00000080  c9 f2 5d 80 49 ec cc ce  aa 07 42 27 64 62 60 be  |..].I.....B'db`.|
00000090  35 73 18 4d 5a b2 97 69  19 6e 4c d1 bc b4 cf 63  |5s.MZ..i.nL....c|
000000a0  fc 34 d0 9b 06 1a ea fe  d6 23 38 8d 15 d2 3c 49  |.4.......#8...<I|
000000b0  be 62 4b e3 2a 29 f6 95  2f 37 5a d3 d1 20 aa df  |.bK.*)../7Z.. ..|
000000c0  2e 86 2a 2a 49 3f 7a 22  d1 67 b1 8b 68 72 05 7e  |..**I?z".g..hr.~|
000000d0  9c 4e 57 a1 97 a0 98 7e  cb 3e 30 b1 a1 9b 19 b3  |.NW....~.>0.....|

чем 0xc0 хуже, чем монада? Совершенно однозначно определяет о чём идёт речь. Мы можем сказать, что 0xc0 является сигнатурой для функции 0xf3253, потому что он однозначно определяет трансформацию 0x6434, осуществляющую 0x643a по отношению к 0x10.

НЛО прилетело и опубликовало эту надпись здесь

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


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


(Заметим, некоторые математические понятия очень интуитивны и вопросов не вызывают при применении в качестве аналогии — те же множества, например).

НЛО прилетело и опубликовало эту надпись здесь

Более новые языки программирования успешно избегают использования монад, предоставляя все преимущества от полезных идей, проистекающих от монад. Тот же раст — весь полон монад (Result, Some, Either, etc), но слово "монада" нигде не встречается. Вместо этого дают приятный сахар (с глубокими архитектурными последствиями) и массу гарантий качества. (тот же ?, который позволяет писать почти-что-bind не ломая мозг).

НЛО прилетело и опубликовало эту надпись здесь

Трейты не нужны для "реализации" типа (если вы про impl). Если вы хотите реализовать стандартные трейты для своего типа — вы это легко можете сделать. Более того, если реализация тривиальная, то можно попросить компилятор сделать самому (derive) из реализаций трейтов для использованных вами типов.

НЛО прилетело и опубликовало эту надпись здесь

Очень просто: в Расте монадического сахара нет, а значит и реализовывать нечего :-)


Забавно, кстати, получается: все хотят монад, но на самом деле всем нужна do-нотация...

НЛО прилетело и опубликовало эту надпись здесь

Не знаю. Вы написали мне простыню на хаскеле и спросили как такое сделать на Rust. Я вашего хаскела не разумею. Скажите, что сделать хотите-то. Параметризировать один тип другим?

Он хочет do-нотацию. Это такой языковой способ избавляться от "лесенки" колбеков и писать код на одном уровне.


Нечто вроде сопрограмм с их оператором await, но с возможностью многократного возобновления с одной и той же точки.

НЛО прилетело и опубликовало эту надпись здесь
Для тех, кто не в теме, что это за возможность такая? Как рассахариваются несколькострочные конструкции, если функция не удовлетворяет естественным квадратам? Или там единственное отличие состоит в отсутствии требования к наличию fmap?
НЛО прилетело и опубликовало эту надпись здесь

Генераторы, у которых выход с одной стороны втыкается во вход с другой?

Теперь уже я вас не понимаю...

НЛО прилетело и опубликовало эту надпись здесь

На самом деле в Rust просто ещё HKT нормальных не сделали. Точнее, сами HKT там уже есть, но к ним желательно бы ещё Higher-Kinded Traits добавить.


Как добавят возможность писать trait на семейство типов — так сразу и монады появятся.

Тот же раст — весь полон монад (Result, Some, Either, etc), но слово "монада" нигде не встречается. Вместо этого дают приятный сахар (с глубокими архитектурными последствиями) и массу гарантий качества. (тот же ?, который позволяет писать почти-что-bind не ломая мозг).

И это очень грустно, ведь раст полон копипасты, условно, map для Option, map для Iterator и так далее. При этом, в некоторых "монадах" одни возможности появляются раньше, чем в других. А для некоторых (async/await) требуется поддержка компилятора, так что даже библиотекой не исправишь. И все это мешает писать по-настоящему обобщенный и абстрактный код, как в хаскеле.


Я сегодня писал около-хеллоуворлд на расте, и столкнулся с неудобством обработки Result даже с "?". Хотел пройти по директории и напечатать содержимое. (См. read_dir).


fn print_entry(entry: Result<DirEntry>) -> Result<()> {
    let path = entry?.path();
    let path = path.to_str().or_not(Error::new(/*skip*/))?;
println!("{}", path);
}
fn main() -> Result<()> {
    for entry in read_dir(Path::new("/")) {
        let _ = print_entry(entry):
    }
}

Чтоб скипать итерацию цикла с ошибкой при помощи оператора ?, пришлось внести кусок в отдельную функцию (ладно, это нормально), результат которой игнорируется (выгдядит как костыль). А чтоб использовать? для Option, а на для Result, пришлось None в Err превращать.


Не исключаю, что сидел было лучше, я в расте нуб. Но пока впечатление такое, во это все далеко не элегантно.

PS. А почему я не использовал map() и bind()? Зациклился, блин, на операторе ?...

А что мешает в print_entry принимать аргументом DirEntry напрямую и писать что-то вроде


for entry in read_dir(Path::new("/") {
    print_entry(entry?);
}

Я хотел просто пропустить те файлы, которые почему-то Err(), а не выходить из функции по первой ошибке.

А, неправильно понял. Ну, тогда


for entry in read_dir(Path::new("/"))?.filter_map(Result::ok) {
    print_entry(entry)
}

или вообще


read_dir(Path::new("/"))?
    .filter_map(Result::ok)
    .for_each(print_dir);

filter_map, for_each, Result::ok

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

ЖЖили были очень интуитивное множества, а потом появился Кантор.

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

НЛО прилетело и опубликовало эту надпись здесь

Бесконечные множества — это уже не интуитивное. Так же как и множества, построенные через предикаты. Перечислимые конечные множества — наше всё.

Конечные множества перечеслимы.


Нет царских путей.

С чего бы? Берем любое невычислимое число, формируем множество из него одного — и вот у нас уже неперечислимое конечное множество.

В этом месте прибегают конструктивисты и задают вопрос: что означает «берём»?
Ну… Это же зависит от нашей интуиции. Если наша интуиция верит в наши бесконечные способности различать любые структуры, тогда да, контринтуитивно. Но почему мы должны верить в наши бесконечные возможности различать? Судя по всему, даже у самой Вселенной эти способности ограничены. Она не способна различать, допустим, координаты электрона, болтающегося на орбите атома.
Я вот в этом вашем ООП никак не могу интуитивно понять, чем декоратор отличается от фасада или адаптера. Или, если спросите, что за паттерн такой, стратегия, я не смогу сказать. Или как канонично писать команду (я вот написал print("meh");, это уже команда?).

Э-э-э… А почему так сложно просто запомнить?


data SomeDecorator a = SomeDecorator a
instance Foo a => Foo (SomeDecorator a)

data SomeAdapter a = SomeAdapter a
instance Foo a => Bar (SomeAdapter a)

data SomeFacade a b c d e = SomeFacade a b c d e
instance Foo a, Bar b, Baz c, Has Qux e, Monad e => Wsx (SomeFacade a b c d e)

"Стратегия" — это то, что вы передаёте в функцию sortBy под видом компаратора


"Команда" же своя в каждой архитектуре. Да, можете считать print("meh") командой (но не можете считать её командой в терминах CQRS или там UI).

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

Ну дык потому что кто же паттерны ООП будет специально объяснять в терминах ФП-то? Обычно как бы считается, что ООП куда понятнее ФП...


Надо в таких случаях брать обычное отображение ООП на ФП, и прогонять паттерны через него (как я и сделал когда писал комментарий выше):


  1. конкретный класс — data type;
  2. интерфейс, он же чистый абстрактный класс — class;
  3. реализация интерфейса классом — instance.
Вообще-то, монада в программировании используется именно в том смысле, в котором она используется в филиосфии. Монада — это нечто единое, потому что основное свойство монады — это умение сливаться воедино. Когда мы можем Конструкцию из Конструкций снова превратить в Конструкцию. Список из Списков просто в Список. Или Операцию с Диском из Операций с Диском снова в единую Операцию с Диском. Это основная механика монады, и она прям почти по словарю философских терминов.
Спасибо, прочитал статью, понял написанное, возможно, буду пользоваться.
Обидно другое: придёт дедфуд, сначала я не пойму его комментарий, а после прочтения порождённой ветки окажется, что или таки не понял статью, или что статья не труЪ :)
требование к категории: для морфизмов обязательно должна выполняться ассоциативная композиция, таким образом, что для морфизма f: A = > B и g: B = > C существует морфизм h = g(f): A = > C.

А есть примеры как это может быть не так? Потому что иначе не очень понятно в чем смысл этого требования…

Смысл требования в том, что оно требуется. Это называется аксиоматической подход.

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

Почему помидор жёлтый? Потому что зелёный. Как-то так. Без требования существования композиции теория сильно обеднится. Структуры в которых композиции стрелок может не быть существуют, пример дали ниже.

То что помидор зеленый когда он желтого цвета — это, не знаю, часть определения помидора, или свойство помидора, или что-то еще, но это не требование к помидорам.

Ниже — это предложение убрать стрелку? Ну так это не пример.
Может я дурак, но я не могу представить такие функции чтобы их нельзя было композировать (при совпадении типов конечно же). И у меня возник вопрос: а так вообще бывает? А можно пример? А мне почему-то вместо ответа предлагают «убрать стрелку» ну, я даже не знаю… Печально.

Просто в теоркате "функции" (т.е. морфизмы, они же стрелки) — это произвольные объекты, удовлетворяющие вот этим самым требованиям, т.е. не обязательно функции.

НЛО прилетело и опубликовало эту надпись здесь
А есть примеры как это может быть не так?

Да легко: просто возьмите картинку из поста и сотрите "лишнюю" стрелочку.


Потому что иначе не очень понятно в чем смысл этого требования…

Потому что морфизм в теории категорий — это обобщение понятия функции, а у функций такое свойство есть, и без этого свойства их исследовать не интересно.

Простите, вы случайно не дипломированный тавтолог?
просто возьмите картинку из поста и сотрите «лишнюю» стрелочку

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

Так если это свойство всех функций, то не надо писать что это «требование». Требование — это то, что может не выполняться, но тогда получится что-то другое. Ну например «чтобы считаться зеленым яблоком, яблоко должно иметь зеленый цвет шкурки. Другое требование к зеленым яблокам — расти на деревьях». Как вам такое «другое требование»? Это не требование, а тавтология. Но действительно, неинтересно исследовать яблоки не учитывая что они растут на деревьях.

Суть моего вопроса в том, что непонятно бывают ли такие функции, что их нельзя скомпозировать.

Категории это не про функции, точнее не только про функции.

Так пример-то можно?

Пример категории где морфизмы не функции или пример структуры без композиции?
Первое — категория, которая получается из частично упорядоченного множества, объекты — элементы этого множества, а стрелка между двумя объектами существует тогда и только тогда, когда один не больше другого.
Второе — три объекта, три единичных стрелки и две стрелки из первого объекта во второй и из второго в третий.

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

Мешает то, что стрелки не функции, они никчему не применяются. И, по условию, того что могло бы претендовать на композицию просто нет.

И в вашем примере не совсем понятно что могло бы помешать применить одну из стрелок из первого во второй, а потом к результату применить стрелку из второго в третий.

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

Это не имеет никакого смысла. Потому что эта стрелочка только символизирует что мы можем сделать двойное преобразование и все будет хорошо.

Ну да, а если мы её уберём — это будет символизировать что мы не можем сделать двойного преобразования. Так вот: если мы не можем сделать двойного преобразования, то у нас уже не категория.


Так если это свойство всех функций, то не надо писать что это «требование».

Это свойство для функций, но требование для морфизмов.


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

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


Или вот вам пример из программирования, на C#:


class Person : NamedObject {
    public string Name { get; set; }
}
interface NamedObject {
    string Name { get; }
}

// ...

void Hello (NamedObject a) {
    Console.WriteLine($"Hello, {a.Name}!");
}

В этом коде класс Person обладает свойством "иметь имя", а интерфейс NamedObject имеет требование "иметь имя". Это требование возникло не потому что у нас вдруг может возникнуть объект без имени (хотя он без проблем может), а потому что не потребовав имя в интерфейсе мы не сможем его использовать в методе Hello. От того, что у интерфейса NamedObject пока что всего одна реализация, требование "иметь имя" не становится тавтологией.

Ну да, а если мы её уберём — это будет символизировать что мы не можем сделать двойного преобразования. Так вот: если мы не можем сделать двойного преобразования, то у нас уже не категория.

Вот я и хочу пример когда у нас есть какие-то A, B и С и какие-то преобразования A->B и B->C, и при этом нельзя из этого собрать преобразование A->C.
Вот я и хочу пример когда у нас есть какие-то A, B и С и какие-то преобразования A->B и B->C, и при этом нельзя из этого собрать преобразование A->C.

Третий раз вам повторяю: морфизм — это не преобразование! С точки зрения теорката это просто стрелочка. У неё нет никаких свойств сверх тех, которые мы потребовали в определении.

Как-бы, понятие категория — это аксиоматическое определение системы «преобразований». Если Вы говорите о преобразованиях, то Вы автоматически говорите о категориях, поэтому автоматически выполняются аксиомы :) Поэтому из преобразований собрать всегда получится. Но категории бывают не только из преобразований (акисоматика категорий, оказывается, применимой очень и очень широко). Морфизмами могут быть не только преобразования. Но, например, и бинарные отношения, числа, слова в конечных алфавитах и так далее, и тому подобное. И в этих системах уже может быть так, что из A -> B и B -> C не всегда можно построить A -> C.

Выше приводили пример с отношением «дружбы».
Урашечки, спасибо, всё встало на свои места.
Тут видимо смутило название «морфизм». В моей голове он почему-то связан с изменением чего-то.
Спасибо за статью, но ее начало производит неверное впечатление, что ФП — это про ТК, про математику и прочий HOTT.

На Хаскеле можно (и нужно) писать, не вдаваясь в ТК вообще, и не пытаясь понять «что такое монада». Этот вопрос — математический, и в контексте Хаскеля не особо помогает. Помогает практика использования монад и какая-никакая, а программистская интуиция, нарабатываемая примерами. Пусть даже некорректная, но достаточная, чтобы писать код на Хаскеле.

Новички, не ведитесь, ТК — это не про Хаскель, это про математику, как бы хаскеллисты ни пытались это представить.

Рекомендую посмотреть доклад Виталия Брагилевского «The clear path to Haskell complexities», там популярно объясняется, что проблемы с изучением Хаскеля — в неверных подходах к обучению.
P.S. Проголосовал «и знать не хочу».
тем кто хочет попробовать функциональное программирование есть аналог функционального языка Scheme называется Перфо.Net
тхаб.рф/wiki/Учебник_языка_Перфо_для_школьников — очень простой
тхаб.рф/wiki/Перфо.NET — исходники языка ~ 1000 строк можно поэкспериментировать добавить свои функции/поменять логику работы

тхаб.рф/wiki/Перевод_терминов_функционального_программирования — здесь я экспериментировал с упрощенными терминами из статьи habr.com/ru/post/505928 «Почему функциональное программирование такое сложное» для упрощения понимания (например мне сильно не нравятся термины которые являются грубыми переводами с английского (например Монада — по моему в языке программирования надо заменить на Контейнер, map — Преобразовать, Морфизм на Преобразование Типов и т.п.). Особенно остро неточный перевод виден при написании учебника, примеров, а потом и кода). Термины д.б. такими — чтобы много не приходилось объяснять что они значат.
Мне кажется что, благодаря Перфо — есть возможность сделать уточнённый перевод терминов и понятий функционального программирования, под них сделать свой диалект языка и учебник по ФП и по функциональному языку. И посмотреть как это будет выглядеть и насколько это будет удобно и эффективно.
Если кому нибудь интересно написать максимально простой БЕСПЛАТНЫЙ учебник по функциональному программированию для школьников/начинающих программистов — пишите в личку
например Монада — по моему в языке программирования надо заменить на Контейнер

Монада — это не контейнер.

Это цитата отсюда habr.com/ru/post/505928
«Ее Величество» Монада – это простой и банальный контейнер. Ее основная цель – обрабатывать данные в контейнере, не вынимая их наружу. Для этого к ней прицепили парочку функций (map). Например, если у нас есть монада-список (массив) чисел, то преобразование их в строки можно сделать прямо в массиве, сразу получив на выходе готовый массив строк, не заморачиваясь с циклами, созданием новых массивов и т.п.
НЛО прилетело и опубликовало эту надпись здесь
Вы меня извините, но я новичок и из Вашего предложения понял слова:
Контейнером для чего является… частично применённых функций r ->? Для ...? Заодно чем… отличаются от… и зачем их разделять?

Я разобрался пока на уровне:
тхаб.рф/wiki/Учебник_языка_Перфо_для_школьников
там разработчик добавил список — list и скоро добавит map — преобразовать или применить — незнаем как назвать

Класс, типа функциональный язык вообще без функций! даже не знал что такие бывают :-)


Давайте вы сначала хоть один нормальный ЯП выучите, а потом уже будете спрашивать про монады?

Зарегистрируйтесь на Хабре , чтобы оставить комментарий