Еще Одно Руководство по Монадам (часть 3: Монадные Законы)

http://mvanier.livejournal.com/4586.html
  • Перевод
By Mike Vanier

В прошлой статье я рассказал о двух фундаментальных монадических операциях класса типов Monad: оператор связывания (bind, >>=) и функция return. В этой статье я закончу с определением класса типов Monad и расскажу о монадных законах.

Полный класс типов Monad


Давайте взглянем на всё определение класса типов Monad:

class Monad m where
    (>>=) :: m a -> (-> m b) -> m b
    return :: a -> m a
    (>>) :: m a -> m b -> m b
    fail :: String -> m a


Мы видим знакомое: оператор >>= и функцию return с теми же типами, но кроме них есть еще оператор >> и функция fail. Что они означают?

Функция fail изначально — очень примитивный способ оповещения об ошибке. Она вызывается, когда оператор >>= не может связать значение типа a и функцию типа a -> m b из-за ошибок сопоставления. Я сейчас не хочу вдаваться в детали этого механизма, потому что это скучно; посмотрите документацию на сайте Haskell, если вам это нужно. В большинстве случаев беспокоиться о fail не нужно.

Оператор >> немного интереснее. У него такой тип:

(>>) :: m a -> m b -> m b


Этот оператор представляет собой монадический оператор последовательности. В частности, это вариант монадического применения (>>= или «bind»), который отбрасывает распакованное значение типа a перед выполнением «действия» типа m b. Он определен следующим образом:

mv1 >> mv2  =  mv1 >>= (\_ -> mv2)


Мы можем видеть здесь, что любое значение, распакованное из монадического значения mv1, отвергается, и потом возвращается финальное монадическое значение mv2. Оператор бывает полезным, когда тип распакованного значения равен (), то есть, является пустым типом. Хорошим примером можно считать функцию putStrLn:

putStrLn :: String -> IO ()


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

putStrLn "This is string 1." >> putStrLn "This is string 2."


И почему же это работает? Посмотрим на типы:

(putStrLn "This is string 1.") :: IO ()
(putStrLn "This is string 2.") :: IO ()


То есть, оператор >> комбинирует два монадических значения типа IO () в одно результирующее монадическое значение типа IO (). Давайте возьмем оператор >> и специализируем его для нашего случая:

(>>) :: m a -> m b -> m b


Если m — это IO, и a, и b(), то получим:

(>>) :: IO () -> IO () -> IO ()


По записи можно сказать, что, вероятно, оператор >> выполняет подряд два «действия» — печать строки.

Теперь более сложный пример. Нам нужно считать строку текста с терминала и дважды ее напечатать. Мы можем сделать это так:

readAndPrintLineTwice :: IO ()
readAndPrintLineTwice = getLine >>= (\s -> (putStrLn s >> putStrLn s))


Из-за приоритетов операторов запись можно оставить без скобок:

readAndPrintLineTwice :: IO ()
readAndPrintLineTwice = getLine >>= \s -> putStrLn s >> putStrLn s


Итак, что это значит? getLine — монадическое значение («действие»), которое считывает строку текста с терминала. Оператор >>= «распаковывает» эту строку из монадического значения и связывает ее с именем s (потому что \s -> putStrLn s >> putStrLn s — это монадическая функция, второй аргумент оператора >>=). Затем строка, названная s, используется монадическим значением putStrLn s >> putStrLn s, которое ее последовательно печатает два раза.

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

Прямо сейчас я собираюсь немного вернуться назад и посмотреть на монадные законы. Они играют большую роль в использовании оператора >>= и функции return для каждой конкретной монады. После этого мы обратимся к более практическим материалам.

Три Закона Монадности


Многие важные законы идут в группах по три: три механических закона Ньютона, три закона термодинамики, Три Закона Робототехники Азимова, три Кеплеровских закона планетарного движения, и так далее, и так далее. Монады в этом не отличаются, ну, конечно, за исключением, что «Три Монадных Закона», важнее всего другого. ;-)

Чтобы оператор >>= и функция return были правильными для определенной монады, они должны иметь корректные типы этой монады. Так, например, определения >>= и return для монады Maybe содержат ее тип:

(>>=) :: Maybe a -> (-> Maybe b) -> Maybe b
return :: a -> Maybe a


А для монады IO содержат тип IO:

(>>=) :: IO a -> (-> IO b) -> IO b
return :: a -> IO b


Однако, этого недостаточно. Эти функции/операторы также обязаны удовлетворять трем «монадным законам». Монадные законы на самом деле очень просты; они призваны гарантировать, что монадическая композиция будет работать предсказуемым образом. Сначала я дам вам «приятную» версию монадных законов, а затем покажу (уродливый) способ, как они обычно описываются. (Скажите мне спасибо: «приятный» вариант куда легче понять.)

Приятная версия

Вот приятное определение трех монадных законов, выраженных в терминах монадической композиции (вспомните, что оператор (>=>) — это монадический оператор композиции функций):

1. return >=> f       ==    f
2. f >=> return       ==    f
3. (>=> g) >=> h    ==    f >=> (>=> h)


О чем эти законы говорят нам?

Законы 1 и 2 говорят, чем должен быть return: это единица (нейтральный элемент) для монадической композиции функций (первое правило утверждает, что return — левая единица, а второе — что правая). Другими словами, композиция монадической функции f и return (в любом порядке) просто возвращает функцию f. Аналогами можно считать 0 — нейтральный элемент для функции сложения целых чисел, и 1 — нейтральный элемент для целочисленной функции умножения; в каждом из случаев нейтральный элемент, соединенный с обычным значением при помощи соответствующей функции, просто вернет назад это значение.

Закон 3 гласит, что монадическая функция композиции ассоциативна: когда мы хотим комбинировать три монадические функции (f, g, h), не важно, какие две мы соединим первыми. Это аналог того, что сложение и умножение тоже ассоциативны в применении к целым числам.

Вам не кажутся эти законы смутно знакомыми? Взглянем на соответствующие «законы», которым удовлетворяет обычная функция композиции:

1. id . f       ==  f
2. f  . id      ==  f
3. (. g) . h  ==  f . (. h)


где id — нейтральный элемент, единица. Уловили сходство? Композиция функции с единицей слева или справа даст снова ту же функцию, и функция композиции ассоциативна. Монадическая функция композиции должна быть ассоциативна, и return должен быть монадическим эквивалентом единичной функции, — чтобы поведение монадической композиции было таким же предсказуемым, как и поведение обычной композиции.

Какое значение у этих законов с точки зрения программиста? Так как мы желаем, чтобы наши монады вели себя разумно, наши определения return и >>= должны удовлетворять этим законам. Мы скоро узнаем, каким образом проверить корректность определений >>= и return. [Заметьте, что монадные законы выражены в терминах оператора >=>, а не оператора >>=, но мы увидим версию с использованием >>=, — она эквивалентна.]

Однако, есть загвоздка: Haskell не проверяет монадные законы! Единственное, что проверяется, — это чтобы типы определений return и >>= были корректными. Выполняются законы или нет, должен проверить программист.

Многие люди спрашивают: «Почему Haskell не может проверить монадные законы?» Ответ простой: Haskell пока еще недостаточно мощный! Для того чтобы получить достаточно мощный язык, который бы доказывал корректность монадных законов, нужно что-то вроде доказателя теорем (teorem prover). Доказатели теорем захватывают воображение, и они, возможно, — будущее программирования, но они гораздо сложнее традиционных языков программирования. Если вам интересно, есть уважаемый доказатель теорем Coq, он доступен здесь. Но в Haskell программист сам должен озаботиться, чтобы монада, которую он написал, не нарушала монадных законов.

Уродливая версия

Проблема приятной версии в том, что оператор >=> не определяется напрямую в классе типов Monad; вместо этого определен оператор >>=, а оператор >=> выводится из него, как я показал выше. Так что если мы ограничиваем определения до операторов >>= и return, нам нужны монадные законы, содержащие только return и >>=. И в таком виде они подаются в большинстве книг и документаций по монадам в Haskell, несмотря на меньшую интуитивность, чем показано в прошлой секции.

В терминах оператора >>= и функции return, монадные законы выглядят так:

1. return x >>= f    ==  f x
2. mv >>= return     ==  mv
3. (mv >>= f) >>= g  ==  mv >>= (\x -> (f x >>= g))


где типы различных значений такие:

mv :: m a
f  :: a -> m b
g  :: b -> m c


для некоторых типов a, b, c и какой-то монады m.

Вывод уродливой версии монадных законов из приятной версии

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

>=> g  =  \x -> (f x >>= g)


Закон 1:

return >=> f            ==  f
\x -> (return x >>= f)  ==  \x -> f x
return x >>= f          ==  f x           -- Q.E.D. ("Что и требовалось доказать")


Обратите внимание, что \x -> f x то же самое, что и просто f.

Закон 2:

f >=> return == f
\x -> (f x >>= return) == \x -> f x
f x >>= return == f x
let mv == f x
mv >>= return == mv — Q.E.D.

Закон 3:

(>=> g) >=> h                 ==    f >=> (>=> h)
\x -> ((>=> g) x >>= h)       ==    \x -> (f x >>= (>=> h))
(>=> g) x >>= h               ==    f x >>= (>=> h)
(\y -> (f y >>= g)) x >>= h     ==    f x >>= (\y -> (g y >>= h))
-- Вычисляем (\y -> (f y >>= g)) x получаем: (f x >>= g)
(f x >>= g) >>= h               ==    f x >>= (\y -> (g y >>= h))
-- Пусть mv = f x, тогда:
(mv >>= g) >>= h                ==    mv >>= (\y -> (g y >>= h))
-- Заменяем g на f, h на g:
(mv >>= f) >>= g                ==    mv >>= (\y -> (f y >>= g)) 
-- Заменяем y на x в правом выражении и получаем:
(mv >>= f) >>= g                ==    mv >>= (\x -> (f x >>= g))   -- Q.E.D.


На шаге вычисления (\y -> (f y >>= g)) x мы просто применяем всю функцию (\y -> ...) к аргументу x; при этом y заменяется переменной x в теле функции (оно обозначено многоточием (...)), и тело функции возвращается как результат. В функциональном языке программирования Lingo эта операция называется бета-редукцией. {1: В данном случае речь идет о разделе математики под названием лямбда-исчисление, где описывается, в том числе, бета-редукция.} Бета-редукция — основной способ вычисления функций. Последний шаг, где происходит замена y на x, корректен потому же, почему следующие две функции:

\x -> f x
\y -> f y


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

Какова идея?

Монадные законы иногда можно использовать в коде, заменив длинное выражение более коротким (например, вместо return x >>= f можно писать просто f x). Однако, мы покажем в следующих статьях, что основная польза монадных законов в том, что они позволяют выводить определения return и >>= для конкретных монад.

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

Do-нотация



Вспомним функцию readAndPrintLineTwice, определенную выше:

readAndPrintLineTwice :: IO ()
readAndPrintLineTwice = getLine >>= \s -> putStrLn s >> putStrLn s


У нее есть одно достоинство: она записывается в одну строку. Недостаток — это не самая легкочитаемая строка в мире. Дизайнеры языка Haskell заметили, что монадические определения часто трудно читать, и придумали действительно приятный синтаксический сахар, с которым определения получаются более читаемыми.

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

-- Форма 1.
-- mv :: m a
-- f  :: a -> m b
 
mv >>= \x -> mf x
 
-- Форма 2.
-- mv  :: m a
-- mv2 :: m b
 
mv >> mv2


Нотация разрабатывалась с намерением сделать эти две формы легкочитаемыми. Она начинается с ключевого слова do, за которым следуют некоторые монадические операции. Так эти два наших примера будут записаны в do-нотации:

-- Форма 1, do-нотация.
do v <- mv
   f v
 
-- Форма 2, do-нотация.
do mv
   mv2


В Форме 1 первая строка значит, что мы берем монадическое значение mv и «распаковываем» его в обычное под названием v. Вторая строка — это просто вычисление f от v. Результат строки f v является результатом всего выражения.

В Форме 2 в первой строке «выполняется» монадическое значение («действие») mv. Во второй строке «выполняется» другое монадическое значение («действие») mv2. Таким образом, мы имеем просто нотацию, которая увязывает в последовательность mv и mv2, как это делает оператор >>.

Компилятор в Haskell преобразовывает удобную do-нотацию в запись без do для Формы 1 и Формы 2. Это просто синтаксическое преобразование, а смысл обеих записей идентичен. Кроме того, обе формы можно смешивать в одном выражении каждой из нотаций. Пример:

-- mv  :: m a
-- v1  :: a
-- f   :: a -> m b
-- v2  :: b
-- mv3 :: m c
 
do    
      v1 <- mv
      v2 <- f v1
      mv3
      return v2


Это в точности то же самое, что и:

mv >>= (\v1 ->
  (f v1 >>= (\v2 ->
     (mv3 >> 
        (return v2)))))


Или без скокбок:

mv >>= \v1 ->
  f v1 >>= \v2 ->
    mv3 >> return v2


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

Кроме того, можно смешивать do-нотацию и обессахаренную нотацию в одном выражении. Вот так:

do v1 <- mv
   v2 <- f v1
   mv3 >> return v2


Иногда это полезно, но может часто стать причиной плохой читаемости кода.

Давайте посмотрим, как наши предыдущие примеры будут выглядеть в do-нотации.

-- Считываем строку, затем печатаем ее.
readAndPrintLine :: IO ()
readAndPrintLine =
  do 
     line <- getLine 
     putStrLn line
 
-- Печатаем две строки, одну за другой.
-- Не функция.
do 
   putStrLn "This is string 1."
   putStrLn "This is string 2."
 
-- Считываем строку и дважды ее печатаем. 
readAndPrintLineTwice :: IO ()
readAndPrintLineTwice =
  do 
     line <- getLine
     putStrLn line
     putStrLn line


Здесь код гораздо легче читать благодаря do-нотации. Интересно, что у нее есть дополнительное преимущество (или недостаток, — смотря, каких взглядов вы придерживаетесь): код в Haskell выглядит императивно! Если мы будем читать код сверху вниз, он похож на императивный язык, у которого вместо присвоения стрелка <-. Скажем, readAndPrintLine можно описать так: «вызываем getLine, чтобы считать строку, которую кладем в переменную line; затем вызываем putStrLn, чтобы напечатать эту переменную.» Это решительно не то, что происходит на самом деле (например, line — не переменная), но читать так можно. Для большого количества кода, который выполняет много действий ввода и вывода, do-нотация — очень удобный способ записи.

У do-нотации есть и другие полезные свойства. Например, вы можете внедрить let-выражения и case-выражения в тело do-нотации, что часто бывает удобным. Я не буду вдаваться в подробности, потому что это рутина, — возьмите любое другое руководство по Haskell для изучения этого момента.

В следующий раз

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

Содержание

Часть 1: основы
Часть 2: функции >>= и return
Часть 3: Монадные Законы
Часть 4: Монада Maybe и монада списка
Поделиться публикацией
Похожие публикации
AdBlock похитил этот баннер, но баннеры не зубы — отрастут

Подробнее
Реклама
Комментарии 11
  • +4
    Для кого все три статьи остались неясны, монады проще понять «на пальцах».

    Пусть есть некоторый алгебраический тип, к примеру:

    data Maybe a = Nothing | Just a

    Мы знаем из чего состоит тип, значит можем на прямую рассмотреть case value of с альтернативами для Just a и Nothing. Исходя из этих знаний, мы можем сделать функцию f::Maybe a -> a, выдав значение по умолчанию для Nothing. Это чистые значения.

    А теперь представим что есть некий алгебраический тип, о котором мы ничего не знаем, только лишь конструктор. Значит f::IO String действительно может быть какой угодно альтернативой в IO, о которой мы ничего не знаем. Это может быть прочтенная строка с консоли, ошибка, что угодно. Заметим, что мы даже не можем предполагать, что значение с типом IO String это действительно какая то альтернатива IO, нет это всегда одно значение, но оно «многолико». Именно поэтому getLine::IO String это значение (функция без аргументов), которое может «прочесть любую строку с консоли» — прочтенная строка будет строкой/ошибкой/etc для наблюдателя (наблюдатель не находиться в «чистом» мире), в самой программе оперируется чистое значение «все возможные варианты IO» (ключевые: суперпозиция, посыл к квантовой физике)

    Раз мы не знаем что есть в IO или в любом другом «неизвестном типе»/монаде, значит нельзя что либо сделать со значением IO a. Для этого и есть оператор применения >>=, который достает а из монадного значения и применяет ее к функции f::a -> IO a если это возможно. Иначе (если к примеру IO String был ошибкой, а не прочитанной строкой) возвращает новое значение IO a, о котором мы ничего не знаем. Именно потому, что >>= может вернуть IO a «в обход» нашей f, f должна возвращать IO a. Т.е. однажды «испачкавшись» в монадах вы увязли до самого конца программы. В функциональной программе нет времени, т.е. нельзя стать наблюдателем и посмотреть что там в монадном значении (unsafe функции, те которые при «исключительных» значениях «не знают что делать» и оставлены на совесть программисту, мы не рассматриваем. это хак малодушных :), это не Haskell), значит нельзя избавиться от монада. На самом деле программа на Haskell всегда, не зависимо от времени, окружающего мира и т.д. отдает IO (), «многоликое» неизвестное значение, и завершается, мгновенно. После работы программы мы в своем мире с side-effects наблюдаем за полученным значением с типом IO () и видим один из «выпавших» вариантов: вывод на консоль, окошки и т.д. Даже если программа работает несколько суток, общается с пользователем и выкачивает чего из интернета, все равно в «чистом мире» Haskell программа уже отработала и вернула нам IO () со всем что мы видим, можем ввести и можем получить результат обратно. Там нет времени, там нет side-effects :)

    Заметим, что зная тонкости внутренней реализации ввода/вывода (или любой сторонней либы, чего угодно), можно написать к примеру hasFailed::IO а -> Bool. Но это совсем не хорошо, т.к. из всего «бесконечного» множества вариантов IO a мы вдруг получили Bool, который всегда True | False, не зависимо от действий внешнего мира и времени. Таких функций быть не должно, это unsafe функции. Но может быть hIsClosed::Handle -> IO Bool, применяемая к IO Handle. Тогда логика скрыта в Handle, если там не что-то еще из бесконечного множество «чего то еще». Получил IO Bool мы можем сделать свою логику f::Bool -> IO SomethingElse или дальше катиться в потоке IO SomethingElse. Это может сносить немного крышу. Что бы это понять попробуйте представить, что ваша программа может дать верные результаты или выпасть с ошибками — это все «известные» результаты; либо уборщица шваброй выдернет питание и все накроется — это «не известные» результаты, одно из не подвластных вам проявлений IO SomethingElse. Функциональный мир при этом остается чист и детерминирован.
    • +2
      только мне эти игры с монадами напоминают запихивание мусора под диван. типа у нас абсолютно стерильная комната, но она бесполезна, ибо в ней ничего нет. а если вам что-то нужно — извольте испачкаться в грязи по самые уши, забравшись под диван. и в нём вы останетесь навсегда, изредка высовывая нос подышать чистым воздухом, чтобы потом обратно окунуться в недетерминированный мир.
      • +3
        Это не так. Весь код на Haskell всегда детерминирован и чист (в рамках логики). К примеру getLine::IO String это всегда одно и то же значение типа IO String, не зависимо от времени или каких либо других сторонних факторов. putStr::String -> IO() всегда возвращает одно и тоже значение типа IO () для одной и той же строки. Выражение:

        (getLine >>= putStr)::IO ()

        в принципе без выполнения, даже на этапе написания кода, всегда будет возвращать значение типа IO (). Детерминизм, type-safety, верификация, все присутствует и никаких поблажек. А потом пользователь перенесет получившееся значение, в свой «не чистый» мир, глянув в него. И тут открылись файлы, прочитались строки, заработали SOAP соединения со всеми случайными сбоями и т.д. «Чистая» программа к тому моменту уже «отработала», выдав одно из бесконечно возможных значений типа IO (). А значение — это один из бесконечно возможных сценариев работы императивной программы со всем вводом и выводом. С некоторыми оговорками можно сказать, что переход из «чистого» мира происходит когда Haskell программа транслируется в C/машинный код (императивный, шаг за шагом код), результат которого наоборот зависит от окружающей обстановки. А монады (типы, о которых мы можем ничего не знать, кроме определенных операций >>=, return и т.д.), позволяют завернуть понятие «все возможные значения/сценарии Х» в некоторое не известное значение монадного типа.

        Не все монады «не известны». Maybe тоже монад (тут важно наличие конструктора типов, операций >>=, return, fail etc) со вполне известными вариантами. Просто монады, помимо других задач, элегантно решают проблемы не детерминированного мира (позволяют не знать о себе ничего).
        • +1
          Фортрановскую программу можно написать на любом языке, но вы заблуждаетесь, если думаете, что это обязательно.
        • +1
          На самом деле, ваше объяснение тоже раскрывает не все. Монады — мир огромный, да… И пока их руками не потрогаешь, не поймешь.

          А IO вообще интересная монада. Если ее правильно использовать, она делит код на слои, что есть хорошо.
        • +2
          Жду следующей части. Я пока не знаю haskell, но интересуюсь функциональным программированием в целом. Очень хороший, интересный, понятный цикл даже для начинающих, таких как я. Монады — одна из наиболее любопытных для меня концепций. Я пытался с разных сторон подходить к изучению этой концепции, и со стороны теории категорий, и с практической стороны, но наиболее ясное представление о том, что же это такое и зачем нужно дали эти переводы :)
          • +1
            Спасибо за отзыв! Будет!
          • +1
            Взгляд питониста: пуристы страдают, но никогда в этом не признаются. Лишь поют мантры о чистоте, верифицируемости, детерминизме. Но реальный мир прёт из всех щелей, а абстракции текут
            • 0
              Я не совсем понимаю, в каком таком негативном ключе вы отзываетесь о чистоте, верифицируемости и детерминизме.
              • 0
                никакого негатива, выше tenshi уже сформулировал «ощущения»
              • +1
                Взгляд со стороны — питонисты занимаются мазохизмом, покрывая юнит-тестами малую часть ошибок, легко обнаруживаемых компилятором хаскеля.

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