кроме оформления императивности

А больше они ни для чего и не нужны. Но и то, что вместо

if ((x=foo()) > 0) {
  if ((x=bar(x)) > 0) {
    x=baz(x);
  }
}

можно написать просто

x = foo | bar | baz;

уже не плохо.

А вот люди говорят, State Transactional Memory можно ещё сделать??

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

Но тут такое дело. По монадам написано уйма туториалов, а народ все равно не понимает. Почему ты решил, что тебе кто-то тут напишет лучше?) Я думаю, что ты все равно ничего не понял из того, что я тебе сейчас тут написал, а я не смог в полной мере выразить то, что хотел написать. Такая вот загадочная штука - монада.

https://www.chrisstucchio.com/blog/2013/write_some_fucking_code.html

Двусвязные списки в СИ (комментарий)

уже знаю, что монады позволяют отделить чистое от нечистого. Но они явно должны уметь что-то ещё. Так вот, что они умеют ещё? Но по сути, а не без самого слова «монады»

по сути: монада это некоторая обобщённая, универсальная модель. объекты модели, которые можно обрабатывать (другими моделями — монад трансформерами), сохраняя инварианты модели, её целостность и непротиворечивость (и какой-то model checking, чтобы обеспечить синтез по этой модели).

монадами можно представить объект в стиле ООП: конструктор это метод 0 жизненного цикла объекта (в начале), деструктор — метод N+1 или -1 (в конце), методы 1..N это обычные методы объекта (аналогично таблице виртуальных функций, VMT).

монадами можно представить актор из ООП в стиле Self, Io, акторов Карла Хьюита, мультиагентное моделирование (ср. смоллток как язык программирования биоклеток в изначальной задумке Алана Кея)

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

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

можно изобразить метаобъектный протокол через рефлексию. а можно изобразить логику второго порядка, примерно с той же целью, что и инварианты класса/метода, предусловия/постусловия метода, ограничения контрактов предка при наследовании предка потомком (аналог принципа LSP подстановки Лисков для контрактного + ООП программировния, подробности см. в книгах по Эйфель Бертрана Мейера).

то есть: логика нулевого порядка — это конкретные значения и переменные. проверки в рантайме. логика первого порядка — это ДНФ/КНФ, булева алгебра над значениями, или предикаты (над типами, типа typecase). логика второго порядка — это дополнительно кванторы всеобщности/существования в эту формулу, дополнение какими-то логическими законами (типа де моргана или логического следования, правил отделения), и прочие утверждения-инварианты — уже не в рантайме, а в компайлтайме.

вот например: если бы каждая строка программы возвращала не отдельные значения (логики нулевого порядка), а multiple-value-bind с тьюплом вида (значение-в-логике-0,значение-в-логике-1,значение-в-логике-2,значение-в-логике-3, ....).

то на этом можно было бы реализовать те же исключения или там сигнальный протокол ошибок — если вернулось значение в логике Х>0, трактовать его как предикат (инвариант, пред/постусловие контракта) в рантайме/компайлтайме программы/метаклассах, компайлтайме метапрограммы, метамодели, model checking.

и всякие «нелокальные передачи управления» гарантированно проверять на все возможные, формализованные инварианты и контракты. то есть, гарантировать статически по модели программы (=монады чего-то там) количество различных веток, трасс.

другая часть определения монады («моноид, в категории ...») означает полезность замкнутных математических объектов, типа кольца, группы. полезна становится, если определить на таких объектах меру и/или предикат по тайпклассам. см. например статью Е.Кирпичёва на fprog.ru про «моноиды, измеримые верёвками».

что происходит: задаётся моноид (или несколько, разного типа), формула типа суммы с накоплением, min, max или ещё какая статистика . используется факт «композиция моноидов тоже моноид». на моноидах задаётся мера, по этой операции. на мере определяется «монотонно возрастающий предикат» (то есть, строб типа «была ложь — стала истина». ищется фронт этого сигнала, значение на котором предикат стал истиной). ещё этот предикат и мера используются в структуре «верёвка» - например строки (тоже моноиды), с быстрыми операциями ибо реализованы как сбалансированное дерево. то есть «верёвка» — дерево, которое можно быстро перебалансировать «разрезы и склейки» (сохранив инварианты балансировки и предиката, то есть: композиция моноидов тоже моноид, предикат на композиции определяется через предикат на элементах и мере моноидов элементов, и т.п.)

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

очень интересная статья, да.

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

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

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

ещё «воистену» интересные возможности открываются, если синтезировать монады монадами через монады (монадическими трансформерами), с гарантированными через model checking свойствами.

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

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

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

короче говоря: монада это модель, которая сохраняет целостность и некоторые свойства (инварианты, контракты в металогиках) модели при преобразовании (что обеспечивает синтез-анализ, а не просто анализ).

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

модель X нужна для того, чтобы изменяя её моделью Y получили целостным образом синтезированную с заданными свойствами модель Z.

где подставить: X=RAII, Y=изменение с ошибками или без ошибок, с исключениями или без Z=«контракт: файлы всегда корректно закрываются — выполнен».

ещё тут неявно получается Y1, Y2 типа «ооп в стиле С++ с деструкторами», «обработка ошибок в стиле исключений в С++» и т.п. детали реализации.

но речь не о деталях, а о наиболее общем принципе — его концепции.

Монада - это один из вариантов ...

... моделей вычислений. и тут либо бы про одну и ту же основную модель вычислений (машину вычислений) и разные расчёты разных моделей на одной и той же машине.

либо про металогики и эквивалентные вычисления — на более других машинах.

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

машин, моделей и логик может быть много всяких разных — поэтому далее два пути: практически/эвристический — в полезные модели и применения, ситуации; или теоретически/абстрактный — в формальные модели, теории, логики, исчисления, model checking и прочие категории высшего порядка.

где-то посредине практика с теорией смыкается, и абстракции становятся менее абстрактными и более конкретными, полезными моделями.

Продайте мне Хаскель

Это вброс!?

«Монада – это просто». Том четвертый.

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

транзакция = «согласованное изменение модели через моделью, моноида через моноид» => монада

уравнение баланса «приход=расход» — инвариант = логический закон = контракт в логике второго порядка (и/или, металогике, логике высшей категории)

предусловие «нельзя списать больше, чем на складе» = тоже инвариант, предикат который используется для model checking при синтезе модели (вычислений, монаде, транзации) списания/продажи.

многозначность уровней «транзакция на уровне записей/на уровне таблиц/на уровне объектов предметной области/на уровне инвариантов, предусловий, постусловий этих объектов или других (интерфейсов компонент) / .../ на уровне подсистем инфосистемы / на уровне подсистем разных учётов (бух/налог/фин/упр/...)»

 — категории логик и интерфейсы компонентов (эндофункторы).

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

с точки зрения полезности: синтезировать инфосистему ИУС из аспектов, компонент на основе теории категорий (см. например докторскую С. Ковалёва,

КОВАЛЁВ Сергей Протасович ТЕОРЕТИКО-КАТЕГОРНЫЕ МОДЕЛИ И МЕТОДЫ ПРОЕКТИРОВАНИЯ БОЛЬШИХ ИНФОРМАЦИОННО-УПРАВЛЯЮЩИХ СИСТЕМ Москва 2013

там как раз про это: комплексировку ИУС из компонент на основе АОП и теории категорий. используется ряд теорем теории категорий с доказательствами, синтез-анализ на основе моделей и теорем.

тоже очень интересная работа — и конкретно-практичная, несмотря на несколько зубодробительных формулировок.

Ну например .? в цшарпе — по сути монада maybe.

Список, по которому можно замапить функцию — тоже монада.

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

ссылка на дисер и презентацию.

дисклеймер рулит :-)))

Это как называть числовые типы кольцами или полукольцами: теоретически правильно, а на практике важно что ими можно копейки считать.

ну, может быть важно ещё то, что например в wheel делить на ноль можно. если его там (это деление) правильно определить.

практически полезное знание, ога-ога :-)))

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

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

откуда вывел своё исчисление.

если бы он вывел его например из формулы x = x + 0 = x+ 0*0 + 0*0 + ... = x + sum 0*0 = x + prod a*b, где a,b — ненулевые (нетривиальные) делители нуля

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

только на этот раз — а) точные значения, если сумма конечна б) активно использовать свойства «делителей нуля» для сокращения выкладок.

может, выкладки получились бы проще.

а на практике важно что ими можно копейки считать.

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

модель вычислений (=монада) обычная с натуральными, ничем не хуже/лучше формулы Эйлера про комплексную экспоненту и единицу (1+0=1+0*0+...) или корня из пи*е пополам или вот «исчисления делителей нуля» или там «дифференциального исчисления», например.

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

в альтернативной истории всё могло бы быть по другому, ога-ога Ж:-)))

Наверное, ты имел в виду Software Transactional Memory?

Монада STM для выполнения сложных составных атомарных операций в много-поточном окружении. Фишка в том, что монада позволяет изолировать такое вычисление от других побочных эффектов. Изоляция достигается за счет строгой системы типов языка Haskell. Благодаря этому можно либо атомарно принять все вычисление как одно целое, либо откатить изменения и попытаться применить их еще раз, потому что есть определенные гарантии чистоты.

Реализация STM в Haskell, вероятно, одна из лучших существующих, если не самая лучшая.

Черт, ну и засрали же тему.

Вся эта писанина анонима - мусор?

ещё про практичность монад

call/cc мне нужен для того, чтобы реализовать в моей IDE инкрементную раскраску файла.

сравни подходы:

1) Е. Кирпичёв и статья на fprog.ru про «инкрементальные регекспы» через «моноиды на верёвках»

2) редактор Yi (емакс на хаскеле) и пост в блоге про инкрементальный парсинг в Yi (также см. статьи)

3) твой подход через call/cc

Спасибо, что пришёл. Давай поподробнее про STM. Допустим, у меня есть уже некая программа... Скажем, императивная программа на Хаскеле. Допустим, программа называется «калькулятор». Императивная, потому что у неё есть состояние (регистр памяти, который M+) и ввод-вывод.

Теперь мы хотим калькулятор с undo, undo хотим сделать на базе STM. Можно ли внедрить в такой калькулятор STM, не переписывая её?

Может быть и шедевр, но явно не проясняет тему, а только запутывает.

Можно ли внедрить в такой калькулятор STM, не переписывая её?

Я правильно понимаю, что эти вопросы обозначают. «Я и близко не понимаю как это работает, у меня есть неправильное представление, но расскажите мне что-нибудь»

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

Попытки рационализации, это в зависимости от того, как реализовано состояние, и зачем вообще тут STM. STM нужно для взаимодействий при многопоточности. Откуда это берется в задаче не ясно. В целом если у тебя состояние было в BaseMonad (IO/STM) то никаких проблем добавить STM не переписывая (ну кроме новой функциональности которая потребовалась) не будет. Если у тебя было interact-like State, то проблемы могут быть.

1) Е. Кирпичёв и статья на fprog.ru про «инкрементальные регекспы» через «моноиды на верёвках»

2) редактор Yi (емакс на хаскеле) и пост в блоге про инкрементальный парсинг в Yi (также см. статьи)

3) твой подход через call/cc

Спасибо за пост.

1. Мне нужен не только лексер, но и парсер. Ты мне скажи, можно ли по статье Кирпичёва сделать рекурсивные регэкспы. Я никогда не дочитал до конца man perlre, но мне не припоминается, чтобы они существовали. А они нужны хотя бы для вложенных комментариев в ЯП.

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

3. Мой подход через call/cc я хотя бы понимаю, у него нет ограничений в общности, я понимаю как его отлаживать, а интерпретатор SBCL с call/cc близится к завершению (тьфу-тьфу).

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

Да, скорее всего. STM и IO идут рядом. Очень часто из вычисления STM возвращается вычисление IO, которое затем применяется. В рамках транзакции мы не можем применить IO, но мы можем его вернуть и применить после транзакции (функция join).

Я правильно понимаю, что эти вопросы обозначают. «Я и близко не понимаю как это работает, у меня есть неправильное представление, но расскажите мне что-нибудь»

Я хорошо понимаю транзакции в не менее чем двух разных СУБД. В своё время я этим себе на хлеб зарабатывал. Также я когда-то читал, как STM устроено в Clojure, но на практике ни разу не пробовал.

Думается, что калькулятор может представлять из себя набор вложенных транзакций или одну транзакцию с «точек сохранения» (savepoints), а UNDO означает откат к одной из них. Я понимаю, как это делается, если состояние калькулятора хранится в БД. Не меняя реализацию калькулятора, я только добавляю операторы начала транзакции, её отмены и отката к точке сохранения.

Можно ли это так же легко сделать в Хаскеле?

Да, в данном случае STM будет «из пушки по воробьям», мне не нужна конкурентность от транзакции, а нужна только атомарность изменений.

Отлично

Отлично, ребята. Хорошо, что затронули тему этого языка. Как раз начал изучать его. Скоро я к вам присоединюсь! А пока не унывайте. Всего хорошего, здоровья!

Кстати, как CrossOver поживает?

Наверное вопрос в том можно ли это сделать в хаскеле с STM, т.к. в хаскеле можно почти все. Вложенные транзакции как они есть - нельзя. Не вложенные и докидывать действия внутрь транзакции можно. Откатиться к safe point можно, но некрасиво, будет выглядеть как отлов исключения. Перевыполнить операции можно.

Если говорить совсем на пальцах, то в STM оптимистичная планировка транзакций. У нас есть специальные переменные мы можем их читать, в них писать, у нас пишется об этом лог, по завершению транзакция коммитится, соответственно если какая-то переменная, которую мы читали поменяла состояние, то мы перевыполняем транзакцию. Из этого следствия: 1. Сложность коммита линейная по сравнению с колвом STM операций 2. Чем длиннее транзакция тес выше шанс рестарта 3. Если много конфликтов то много лишней работы. 4. Нельщя выполнять произвольные эффекты в транзакции (можно конечно но это очень небезопасно)

Из хорошего RTS может отлавливать случаи когда транзакцию нужно точно рестартовать и делает это заранее, в случае если транзакция сама сделала retry, то поток не будет перезапущен пока не изменилось состояние переменных которые читали.

Надеюсь этой информации будет достаточно : )

Тогда IORef и atomicModifyIORef'. Внутри какой-нить ExceptT или LogicT в зависимости от того что именно нужно.

CrossOver поживает неплохо и я в нём тоже ничего поживаю.

У нас есть специальные переменные мы можем их читать, в них писать,

Вот. То есть, я должен при переходе на STM найти все побочные эффекты над данными, подлежащие откату, и вручную их поменять? Или можно как-то сказать «а вот теперь вокруг всего этого пусть будет STM». Про вложенность неважно. Пусть будет один уровень UNDO.

Это я не придираюсь, это важный вопрос по технологичности.

И получается укладываться в пять дней, да еще с трекером? Читал, что некоторые при такой системе даже по выходным дорабатывают.

Думаю, что такие откаты придется самому реализовывать. Это если для Undo. STM решает довольно узкую задачу. Там есть откаты, но сильно вряд ли они подойдут для Undo калькулятора. Я думал, что вопрос был вообще, а можно ли приделать сбоку STM?

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

HKT это куда больше, чем просто монады. Держи статью: https://gist.github.com/CMCDragonkai/a5638f50c87d49f815b8
Кроме HKT есть множество других крутых штук. Например, зависимые типы: http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#dependent-types В хаскель уже добавили базовую их поддержку.

Вот тебе ещё обзор по всякому разному, что есть в хаскеле: http://dev.stephendiehl.com/hask/

Думаю, что такие откаты придется самому реализовывать.

Ну почему не подойдут. Пусть у нас есть несколько глобальных переменных, к-рые определяют состояние. Можем мы их запихнуть в STM и сказать, что UNDO - это rollback, а начало следующей операции - это commit? На SQL так можно было бы сделать (только были бы не переменные, а записи в таблице).

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

Не нравится мне это. Просто присматриваюсь к ним.

Это сильно зависит от твоего нынешнего трудоустройства. В целом я считаю это нормальным - честно работаешь и получаешь что заработал. Хотя конечно то, что они следят за временем, которые ты сидишь за компом и считают нажатия на кнопки, означает, что ты не можешь пойти погулять на улице и подумать.

В книге Parallel and Concurrent Programming in Haskell утверждается, что «транзакционная память» - неудачный термин. Это скорее об атомарных операциях чтения/записи переменных. Добавлю от себя, что то, что там создается журнал откатов - это лишь деталь реализации. Поэтому лучше не проводить больших аналогий с транзакциями баз данных. Что-то похоже, но не более того.

Хотя у STM есть приятные фишки, как неявная модель слушатель-источник события, реализованная на уровне run-time языка, а также безопасность относительно асинхронных исключений, т.е. с ними заморачиваться не надо особо.

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

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

И насколько понимаю, undo не будет в STM. Есть либо успешное выполнение (commit), либо есть откат и повторная попытка (retry), а потом еще раз откат, и еще, пока не выйдешь при успешной попытке.

Функции отсюда: https://hackage.haskell.org/package/stm-2.4.4.1/docs/Control-Monad-STM.html

atomically $ do
   something 
   catch inner handler -- сделали safe point
  where
    inner = do
      b <- something
      if b
      then foobar
      else throwSTM Rollback -- откатились

Соответственно типами исключений и хендлерами мы можем делать любую логику отката.

Но тут врятли это нужно. Вообще dave по делу про STM и зачем оно написал.

Возможно catchSTM и throwSTM, вторым можно обрывать транзакцию, первое отменяет действие второго и позволяет сделать recovery. Соответственно все (кроме лога?) что внутри catchSTM при throw будет отменено. Таким образом можно реализовать undo. Результат транзакции другим потокам до коммита будет не виден.

Такая вот загадочная штука - монада.

вспоминается фильм «дежавю» и арка про синкопу

С помощью catchSTM создается safe point в журнале откатов? То есть, в твоем примере при кидании Rollback внутренний something откатится, а первый something сохранится? Где об этом можно почитать?

ЯННП. Лор, это нормально?

Что с логом не знаю , т.е. если у нас:

catchSTM $ readTVar foo >>= \case of True -> throwSTM Rollback ; False -> ..

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

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

Если совсем Н то не очень, тут и понятные вещи были.

я когда-то честно-честно пытался понять что такое

1) монада
2) функтор
3) лямбда-функции и выражения
4) замыкания
5) и прочие странные термины

и ННП. Т.е. отчасти кое-что понял, но потом забыл и опять по кругу.

Сам-то я С погромист.