Pull to refresh

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

Reading time 13 min
Views 7.7K
Original author: Mike Vanier
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 и монада списка
Tags:
Hubs:
If this publication inspired you and you want to support the author, do not hesitate to click on the button
+22
Comments 11
Comments Comments 11

Articles