Кирпичёв правильно пишет про небрежность интуитивного понимания императивных языков:
http://antilamer.livejournal.com/300607.html.
Однако, мне кажется, что важно было бы озвучить, что всё то, что сейчас скрывается под именем "монада" -- само по себе достаточно спутанно в плане педагогики и евангелизма. Классическая шутка SPJ/Вадлера звучит как "нам следовало назвать ЭТО warm fuzzy things, чтобы не пугать людей теоркатом". Шутка поразительно недальновидная. Проблема лежит в той же плоскости, что и называние стоящих перед тобой задач словом "stuff" (это то, с чем борется Аллен в своём GTD).
Монады в настоящий момент являются миру как сложный ком из исторически обусловленных причин, проблем, решений, технических возможностей и теоретических основ (как алгебраических, так и аспектов теории вычислений).
Все эти наслоения можно (и нужно) расщепить в первом приближении так (порядок приблизительно случайный):
- стремление к экспликации эффектов (чистое внедрение императивно-подобных моментов в вычисление), (см. труды Вадлера); здесь мы включаем ввод-вывод, STM, параллельные вычисления и проч.)
- удобный механизм для материализации базовых микро-стратегий вычисления -- вызов функции (call-by-name/call-by-value), многозначность, смена состояния (присваивания!), обработка исключений, останов при неудаче, continuations, бэктрекинг;
- typeclasses как механизм внесения монад в язык, и как следствие -- удобный механизм для мета-перехвата вычисления (невероятно удобно для domain-specific embedded languages);
- строгая проверка типов, проистекающая из использования typeclasses, и позволяющая механически проверять корректность использования объектов;
- существование монадических законов, в которые укладываются монады, что позволяет материализовывать абстрактные комбинаторы; это позволяет находить порой неожиданные изоморфизмы между различными предметными областями, а также помогает при оптимизации и верификации программ;
- проработанная теоретическая основа (теория категорий), на которой базируются монады; это облегчает жизнь создателям базовых библиотек, на которых потом базируется всё реальное программирование;
- монады -- лишь один из классов в длинной цепочке интересных алгебраически обусловленных классов, некоторые из которых слабее монад, а некоторые -- сильнее: Functor, Applicative, Monoid, Traversable, Foldable, Monad со товарищи, Arrow со товарищи;
- стремление к материализации некоторых видов вычислений в алгебраическую структуру (моноидальные вычисления); это открывает широкий простор для оптимизаций, верификации программ, создания абстрактных комбинаторов, а также устранение unbounded recursion -- по мощности результатов это похоже на то, как когда-то ввод-вывод был надежно изолирован в IO Monad;
Потратим по паре абзацев на каждый пункт.
Экспликация эффектов. Clean первым (ЕМНИП) справился с тем, чтобы уложить ввод-вывод в экосистему чистого ленивого языка. Ввод-вывод -- лишь первый эффект, с которым справились таким образом. Сейчас всё, что не укладывается в чистоту и ленивость, оформляется в виде эффектов: транзакции (и их взаимодействие с вводом-выводом), генераторы случайных чисел, синхронизация при параллельных вычислениях). Кроме того, что связано с внешним миром, сюда также идут вычисления, которые не укладываются в родную семантику языка -- например, строгое вычисление аргументов функций (как во всех императивных языках).
Эффекты позволяют беспокоиться только о четком ограниченном подмножестве проблемы, ведь всё что вне эффектов -- это очень "простые" вещи, которые не могут "навредить" -- там нет deadlocks, там не надо думать о барьерах и порядке вычисления. Чудовище, таким образом, загоняется в клетку.
Базовые микро-стратегии вычисления. Не забываем, что люди, стоявшие у истоков Haskell, в первую очередь были заинтересованы в программировании самого компилятора. С помощью монад можно эксплицировать все базовые процессы, происходящие при вычислении -- вызовы функций с разными методами передачи аргументов, лексическую и динамическую вложенность переменных (Env), обработку исключений, выразить присваивание через машину состояний (State), неоднозначные вычисления (amb/List), вычисления с неудачей (Maybe/Error), continuations (Cont), бэк-трекинг.
Отдельной областью исследований были также модульные интерпретаторы, реализованные через монады и сопутствующие monad transformers. Такая конструкция позволяла конструировать интерпретатор нужного языка (например, арифметика + вызов функций + неоднозначность) простым комбинированием отдельных компонентов интерпретатора. Каждый отдельный компонент изолирован от остальных и позволяет раздельную разработку.
Понятно, что такой подход позволяет один раз написать соответствующий блок, проверить его, и использовать для любой задачи, требующей создания интепретатора или даже компилятора).
3. S. Liang, P. Hudak "Modular Monadic Semantics", 1998 http://flint.cs.yale.edu/trifonov/cs629/modular-monadic-semantics.pdf
Механизм для мета-перехвата вычислений. Монады в Haskell реализуются через typeclasses, которые чем-то похожи то ли на interfaces в Яве, то ли на concepts в C++. Typeclasses совершенно ортогональны монадам! Typeclasses позволяют "перехватить" вычисление в другой тип результата.
Например, можно написать на Haskell функцию для вычисления корней квадратного уравнения. Её можно вычислить, передав ей три аргумента -- тогда она вернет пару корней. С помощью typeclasses можно "вычислить" эту функцию в другом контексте так, что результатом вычисления будет код на JavaScript, который представляет собой JavaScript-функцию, вычисляющую корни квадратного уравнения.
Таким образом, можно отделить разработку базового алгоритма от способа его вычисления.
Активно развивающейся областью сейчас является написание DSL для параллельных вычислений. Можно написать на Haskell векторизованный алгоритм, к котором потом написать ряд бэкендов: для SSE, для CUDA, для обычного C, для любой другой векторизующей технологии, которая ещё не появилась. Естественно, алгоритм этот можно попросту вычислять прямо из Haskell, чтобы отлаживать его принципиальную корректность.
Монадические законы, теоретические основы, младшие и старшие братья монад. Обеспечивают возможность формально доказать некоторые базовые вещи, чтобы быть хоть сколько-то уверенным в том, что фундамент не подведет. Это интересно не только авторам самых базовых библиотек, но и тем, кто добрался до задач с такой сложностью, когда каждая возможность автоматической самопроверки приветствуется с энтузиазмом.
Вместе со строгой проверкой типов это позволяет ловить ситуации, когда задача недопонята, сформулирована противоречиво, или просто сложнее, чем кажется. Также это позволяет развивать программу, резко снижая вероятность внесения ошибочных изменений. Так, Galois в своей презентации говорят, что постоянно пытаются закодировать те или иные требования к коду в виде сигнатуры типов.
Также формальная структура (в том числе в моноидальном стиле) открывает широкий простор для оптимизаций на уровне компилятора (в том числе, управляемых программистом через механизм rules). Некоторые жёстко структурированные функции удаётся соптимизировать максимально близко к машинному коду, при этом не жертвуя абстрактностью исходного кода.
![[info]](http://l-stat.livejournal.com/img/userinfo.gif){kind=small}
squadette's journal
