Еще Одно Руководство по Монадам (часть 4: Монада Maybe и монада списка)

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

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

Монада Maybe



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

data Maybe a = Nothing | Just a


Здесь указано, что Maybe — это конструктор типа, в который помещается определенный тип a, чтобы получить (конкретный) тип данных. Еще говорят, что Maybe — это «полиморфный» тип данных, смысл тот же. Так, если бы a был Int, мы бы получили:

data Maybe Int = Nothing | Just Int


Только вот нам не нужно это писать непосредственно, так как абстрактное определение выше подходит ко всем типам.

Значение типа Maybe a может либо быть, либо отсутствовать. Если значение равно Nothing («Ничто»), то его «как бы и нет», а если оно равно Just x для некоторого значения x, то это «просто» значение x. Можно думать об этом как о контейнере, в котором либо 0 элементов, либо он один. (Вспомните: я когда-то говорил, что монадические значения иногда ошибочно представляются в виде контейнеров. Это тот самый случай.)

Полиморфный тип Maybe полезен тем, что мы можем использовать его как модель «расширенной функции», которая либо производит что-то как выходное значение, либо терпит в этом крах и не может вернуть никакое значение. (То есть, такая функция может провалиться.) Это записывается так:

:: a -> Maybe b


Функция f берет значение типа a и либо возвращает Nothing (признак неудачи), либо значение Just x, где у x тип b. Функции вроде f будут работать в монаде Maybe, и композиция двух таких функций выглядит следующим образом:

:: a -> Maybe b   -- предполагаем, что f где-то определена
:: b -> Maybe c   -- предполагаем, что g где-то определена
 
:: a -> Maybe c   -- монадическая композиция f и g
= f >=> g         -- вспомним: >=> - это оператор монадической композиции


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

instance Monad Maybe where
  (>>=)  = {- определение >>= для Maybe -}
  return = {- определение return для Maybe -}


Как мы можем задать (>>=) и return для Maybe?

Сначала напишем каркас определения для >>=, покрывающий два возможных случая левого операнда типа Maybe a:

Nothing >>= f  =  {- нужно дописать -}
Just x  >>= f  =  {- нужно дописать -}


где x имеет тип a. Левую часть определения можно написать и по-другому:

(>>=) Nothing  f  =  {- нужно дописать -}
(>>=) (Just x) f  =  {- нужно дописать -}


Но лучше все-таки, если оператор (>>=) задан как оператор, а не как функция, и Haskell нам это позволяет.

Для завершения этого определения подумаем, что мы хотим получить от монадической композиции в монаде Maybe. Давайте возьмем наш пример с функциями f и g, монадически их скомпонуем и получим функцию h:

:: a -> Maybe b
:: b -> Maybe c
:: a -> Maybe c
= f >=> g


Если мы передадим аргумент в функцию f, и она вернет Nothing (то есть, потерпит неудачу), то что должна вернуть функция h?

f x = Nothing
h x = (>=> g) x = ???


Кажется очевидным, что если f x вернет Nothing, то и h тоже должна вернуть Nothing, поскольку если часть выражения (функция f) не смогла вернуть результат, то и все выражение (функция h) не сможет его вернуть. Единственный вариант, когда h возвращает значение, это когда f вернет результат (назовем его y), он будет передан функции g, и g y — тоже будет корректный результат. Если провалится f или g, то и h завершится неудачей, то есть, вычислением h x будет Nothing.

Имея это в виду, из нашего определения h получим:

= f >=> g
= \x -> (f x >>= g)  -- эквивалент (из определения >=>)
h x = f x >>= g        -- эквивалент
-- предположим, что f x == Nothing
h x = (Nothing >>= g)
    = Nothing
-- таким образом:
Nothing >>= g = Nothing


Теперь мы знаем, как оператор (>>=) реагирует на аргумент Nothing, — он просто возвращает тот же Nothing:

Nothing >>= f  =  Nothing
Just x  >>= f  =  {- нужно дописать -}


Обратите внимание, я здесь заменил g на f, и это корректно, ведь имена функций не важны. На практике мы вообще избавляемся от имен функций, если это возможно, и заменяем их специальным оператором _ (нижнее подчеркивание), вот так:

Nothing >>= _ =  Nothing


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

Теперь давайте подойдем с другой стороны. Если f x не провалится, результатом будет значение Just y для некоторого y. Нам нужно «распаковать» значение y из Just y, которое мы бы потом передали функции g, и g y — это результат всей функции h:

= f >=> g
= \x -> (f x >>= g)  -- эквивалент (из определения >=>)
h x = f x >>= g        -- эквивалент
-- предположим, что f x == Just y 
h x = (Just y >>= g)
    = g y


Что дает нам вторую часть определения:

Nothing >>= f  =  Nothing
Just x  >>= f  =  f x


Заметьте, что я заменил y на x и g на f. Опять же, имена переменных и функций не имеют значения до тех пор, пока вы последовательны.

На этом завершается определение оператора >>= для монады Maybe. Теперь нам нужно получить return для этой монады:

return x  =  ???


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

return x  =  Nothing


для любого x. Однако мы бы нарушили монадные законы, если бы так сделали:

return x >>= f  ==  f x
Nothing >>=  f  ==  f x
Nothing         ==  f x   -- НЕВЕРНО!


Предполагая, что по крайней мере некоторые f x не Nothing (например, рассмотрим монадическую функцию f x = Just x), получим ошибку. Есть и другой вариант:

return x  =  Just x


и он удовлетворяет монадным законам:

return x >>= f
  = (Just x) >>= f   -- по определению return для монады Maybe
  = f x              -- по определению >>= для монады Maybe
                     -- выполнение первого монадного закона
 
Just x >>= return
  = return x         -- по определению >>= для монады Maybe
  = Just x           -- по определению return для монады Maybe
                     -- выполнение второго монадного закона
 
Nothing >>= return
  = Nothing          -- по определению >>= для монады Maybe
                     -- выполнение второго монадного закона


Раз законы соблюдаются, этот вариант и возьмем. Полное определение монады Maybe выглядит так:

instance Monad Maybe where
  return x  =  Just x
 
  Nothing >>= f  =  Nothing
  Just x  >>= f  =  f x


Вау! Мы только что создали нашу первую монаду!

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

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


Сначала проверим закон для случая, когда mv = Nothing:

(Nothing >>= f) >>= g             -- с левой стороны
  = Nothing >>= g                 -- по определению >>=
  = Nothing                       -- по определению >>=
 
Nothing >>= (\x -> (f x >>= g))   -- с правой стороны
  = Nothing                       -- по определению >>=


Хорошо, проверка прошла успешно. Теперь посмотрим, работает ли он для mv = Just v, где v — некоторое значение:

((Just v) >>= f) >>= g            -- с левой стороны
  = f v >>= g                     -- по определению >>=
 
(Just v) >>= (\x -> (f x >>= g))  -- с правой стороны
  = (\x -> (f x >>= g)) v         -- по определению >>=
  = f v >>= g                     -- нормальное применение функции (бета-редукция)


И тоже успешно. Значит, закон выполняется! Это действительно правильное определение монады Maybe! И публика сходит с ума!

В чем смысл всего этого? Это значит, что теперь мы легко можем соединить кучу монадических функций монады Maybe. Вы, возможно, задаетесь вопросом, почему это важно? Совсем нетрудно представить себе много монадических функций в монаде Maybe, то есть, таких, которые могут провалиться. Скажем, пусть у них будет тип Int -> Maybe Int. Вот три подобных функции:

:: Int -> Maybe Int
f x = if x `mod2 == 0 then Nothing else Just (2 * x)
 
:: Int -> Maybe Int
g x = if x `mod3 == 0 then Nothing else Just (3 * x)
 
:: Int -> Maybe Int
h x = if x `mod5 == 0 then Nothing else Just (5 * x)


Нам бы хотелось соединить их в одну функцию, которая есть результат применения по порядку f, g, h:

:: Int -> Maybe Int


И если какая-то из трех функций потерпит неудачу, функция k должна вернуть Nothing. Эта функция умножает входное число на 30, если оно не делится целочисленно на 2, 3 или 5 (а если делится, функция возвращает Nothing).

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

= f >=> g >=> h


Или можете взять оператор >>=:

k x = f x >>= g >>= h


Или, возможно, вам нравится do-нотация:

k x = do y <- f x
         z <- g y
         h z


Это просто, как ни крути. {1: В оригинале — устойчивое выражение «Any way you slice it», аналогичное по смыслу. — Прим. пер.}

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

k x = case f x of
        Nothing -> Nothing
        Just y  -> case g y of
                     Nothing -> Nothing
                     Just z  -> h z


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

f11 = f1 >=> f2 >=> f3 >=> f4 >=> f5 >=> f6 >=> f7 >=> f8 >=> f9 >=> f10


или (с использованием >>=):

f11 x = f1 x >>= f2 >>= f3 >>= f4 >>= f5 >>= f6 >>= f7 >>= f8 >>= f9 >>= f10


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

Монада Maybe очень полезна для пояснения базовых концепций, но она может сбить с толку: многие люди ошибочно верят, что единственная роль монад в обработке нефункциональных вычислений, то есть, тех вычислений, которые работают с вводом/выводом (с консолью или с файлом), с изменяемым глобальным состоянием, и так далее. А я показал, что некоторые монадические вычисления могут быть с тем же успехом выполнены совсем без монад. Получается, что монады не что-то обязательное, они просто очень удобны. Именно поэтому я говорил, что даже несмотря на первоначальную причину изобретения монад для нефункциональных вычислений (работа с IO), у них, как оказалось, гораздо большая применимость. Из-за этого монады хороши.

А теперь перейдем к следующей монаде.

Монада list (список)



Если монада Maybe вам просто понравилась, то монаду list вы даже полюбите. ;-) В данном случае мы заполним следующее определение:

instance Monad [] where
  (>>=)  = {- definition of >>= for lists -}
  return = {- definition of return for lists -}


Заметьте, что для представления пустого списка [] мы используем списковый конструктор типа. Это небольшой хак (для списков в Haskell вшита специальная синтаксическая поддержка). Но ничего не поделаешь.

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

:: a -> [b]


(где [b] значит, конечно, «список элементов типа b»). Вспомните, что обобщенное определение монадической функции записывается следующим образом:

:: a -> m b


для некоторой монады m, которая должна быть конструктором типа. Список — очевидный кандидат в монаду, поскольку «список из» — это конструктор типа (пусть даже его синтаксис жестко зашит в Haskell); по желанию, мы могли бы определить список сами:

data List a = Nil | Cons a (List a)


Тип монадическая функций для него выглядел бы соответственно:

:: a -> List b


Но мы будем все-таки придерживаться стандартного синтаксиса.

Чем являются функции подобного сорта? Обычно их понимают как функции, которые берут входное значение типа a и производят кучу значений типа b, собранных в один удобный контейнер (список). (И опять у нас монада, которая выглядит как контейнер.) Другой способ думать о них как о функциях, возвращающих множество значений, то есть, такие функции возвращают кучу разных значений «в одном». (Я не имею в виду «параллельно», потому что это подразумевает параллельную обработку, чего здесь нет.) Множественные выходные значения — это просто элементы списка. При использовании функций наподобие следующих открываются полезные перспективы:

:: Int -> [Int]
:: Int -> [Int]


Здесь и f, и g принимают одно Int-значение и возвращают много Int-значений. А что если мы хотим взять каждый результат функции f и применить его к каждому результату функции g, коллекционируя результаты применения? Было бы здорово, если бы это можно было сделать непосредственно, без распаковки каждого элемента из списков-результатов функций g и f. И это можно сделать с помощью монады списка.

Давайте перейдем к более материальным примерам этих функций:

:: Int -> [Int]
f x = [x-1, x, x+1]
 
:: Int -> [Int]
g x = [-x, x]


Как же нам «скомпоновать» эти две функции? f x возвращает список, и для применения g к каждому элементу нам нужна функция map:

10   -->  [9, 10, 11]
map g (10)  -->  [[-9, 9], [-10, 10], [-11, 11]]


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

-- Обратите особое внимание на тип concat: [[a]] -> [a]
concat (map g (10))  -->  [-9, 9, -10, 10, -11, 11]


Мы получили набор всех результатов, произведенных через применение f к целому числу и затем применив g к тому, что получилось после f. Если вы думаете об f и g как о функциях, которые создают множество результатов «здесь и сейчас», их выходные значения будут множеством всех возможных применений сначала функции f, а затем функции g. Мы можем представить это в виде диаграммы:

                  g   |  -9
           |  9 ----> |
           |          |   9
           |
       f   |      g   | -10
  10 ----> | 10 ----> |
           |          |  10
           |
           |      g   | -11
           | 11 ----> |
                      |  11


Хорошо видно, что композиция f и g — это множество всех путей между f и g.

Любопытно, что мы только что определили оператор >>= для монады списка! Он задан так:

-- mv :: [a]
-- g  :: a -> [b]
mv >>= g = concat (map g mv)


где mv — это монадическое значение в монаде списка (которое просто список значений типа a). В предыдущем примере mv — это результат вычисления f 10. Определение работает даже для пустого списка [], поскольку отображение (mapping) функции на пустой список даст пустой список, и concat для пустого списка тоже всегда пустой список. Получилось очень простое определение оператора >>=.

[Заметка для фанатов GHC: Я верю, что оператор >>= в компиляторе GHC реализован более эффективно и по-другому, хотя и делает то же самое.]

Как задать return для этой монады? Давайте подумаем о монадическом значении-списке как о «действии», возвращающем много значений. Вспомним, что return должен быть эквивалентом единичной функции, — как и в других монадах. Что будет эквивалентом единичной функции в монаде списка? Она должна брать значение и возвращать «действие», которое после «вычисления» просто вернет это значение. Так мы поняли, что return не может просто возвращать пустой список. Разумно предположить о return что-то такое:

return :: a -> [b]
return x = [x]


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

-- f :: a -> [b]
-- x :: a
return x >>= f  =  concat (map f (return x))   -- по определению >>=
                =  concat (map f [x])          -- по определению return
                =  concat [f x]                -- по определению map
                =  f x                         -- по определению concat
                   -- выполнение первого монадного закона
 
-- mv :: [a]
mv >>= return   =  concat (map return mv)      -- по определению >>=
                =  concat (map (\x -> [x]) mv) -- по определению return
                -- Два случая:
                -- Случай 1:  mv == []
                =  concat (map (\x -> [x]) []) -- по определению mv
                =  concat []                   -- по определению map
                =  []                          -- по определению concat
                =  mv                          -- по определению mv
                -- Случай 2:  mv == [v1, v2, ...]
                =  concat (map (\x -> [x]) [v1, v2, ...])  -- по определению mv
                =  concat [[v1], [v2], ...]    -- по определению map
                =  [v1, v2, ...]               -- по определению concat
                =  mv                          -- по определению mv
                   -- выполнение второго монадного закона


Ну что ж, два закона для монады доказаны. Возможно, вам захочется попробовать другие определения return (когда return возвращает, например, конкретный список [0, 2, 3], или когда возвращает бесконечное количество копий своего аргумента), и вы увидите, что они все будут нарушать монадные законы. Это хороший способ попрактиковаться с монадными законами.

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

-- Третий монадный закон (приятная версия):  
(>=> g) >=> h  =  f >=> (>=> h)
-- По определению: 
>=> g = \x -> f x >>= g
-- Возьмем определение >>= для монады списка:
>=> g = \x -> concat (map g (f x))
-- Можно переписать выражение через оператор композиции (.):
>=> g = concat . map g . f


Кроме того, я воспользуюсь несколькими свойствами функций concat и map. Вам пока придется принять их на веру; потом я покажу, как их получить:

-- уравнение 1:
map (. g)  =  map f . map g
-- уравнение 2:
map f . concat =  concat . map (map f)
-- уравнение 3:
concat . concat  =  concat . map concat


Я как-то уже говорил, что точка (.) является (чистым) оператором композиции. У нее меньший приоритет, чем у применения функции, следовательно, выражения вроде map f. map g значат лишь (map f). (map g). Программисты на Haskell обычно избавляются от скобок, где это возможно. Также важно понимать, что, например, функция map f — это функция map, у которой вообще-то два аргумента (такие: функция для элементов списка и сам список). Если вы вспомните, что я рассказывал про карринг, то вы догадаетесь, что map f — это функция, которая принимает один список и возвращает другой, где к каждому элементу применена функция f. Каррингом мы теперь будем много пользоваться.

Итак, вывод доказательства с учетом всего сказанного:

(>=> g) >=> h
  = (concat . map g . f) >=> h                     -- по определению >=>
  = concat . map h . (concat . map g . f)          -- по определению >=>
  = concat . map h . concat . map g . f            -- удаляем ненужные скобки
 
>=> (>=> h)
  = f >=> (concat . map h . g)                     -- по определению >=>
  = concat . map (concat . map h . g) . f          -- по определению >=>
  = concat . map ((concat . map h) . g) . f        -- эквивалентное преобразование
  = concat . (map (concat . map h)) . (map g) . f  -- по уравнению 1
  = concat . map (concat . map h) . map g . f      -- удаляем ненужные скобки
  = concat . map concat . map (map h) . map g . f  -- по уравнению 1


Теперь нам нужно показать, что:

concat . map h . concat  =  concat . map concat . map (map h)


Давайте это докажем.

-- добавим скобки для ясности:
concat . (map h . concat) = concat . map concat . map (map h)
-- по уравнению 2:
concat . concat . map (map h)  =  concat . map concat . map (map h)
-- добавим скобки для ясности:
(concat . concat) . map (map h)  =  concat . map concat . map (map h)
-- по уравнению 3:
concat . map concat . map (map h)  =  concat . map concat . map (map h)


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

Заметка на полях: Вывод тождеств с map/concat (уравнения 1, 2 и 3)

Подготовка

Прежде чем приступать к доказательствам тождеств, нам сначала надо доказать несколько других (математика трудна!). Перечислим их:

-- Выражение 4:
concat (x:xs) = x ++ concat xs
-- Выражение 5:
concat (++ y) = concat x ++ concat y
-- Выражение 6:
map f (++ y) = map f x ++ map f y


Выражение 4 следует из определения concat. Выражение 5 легко доказать через индукцию по x с использованием уравнения 4.

-- базовый случай: x - пустой список
concat ([] ++ y) = concat [] ++ concat y
concat y = [] ++ concat y  -- по определению concat []
concat y = concat y        -- по определению ++
-- Верно.
 
-- индукция: список x не пустой; x1 - голова списка; xs - хвост списка.
concat ((x1:xs) ++ y) 
  = concat (x1 : (xs ++ y))      -- по определению ++
  = x1 ++ concat (xs ++ y)       -- по уравнению 4
  = x1 ++ concat xs ++ concat y  -- inductive hypothesis
 
concat (x1:xs) ++ concat y
  = x1 ++ concat xs ++ concat y  -- по уравнению 4
-- Верно, что и требовалось доказать.


Уравнение 6 можно доказать таким же образом:

-- базовый случай: x - пустой список
map f ([] ++ y) = map f [] ++ map f y
map f y = [] ++ map f y
map f y = map f y
-- Верно.
 
-- индукция: список x - не пустой; x1 - голова списка; xs - хвост списка.
map f (++ y)
  = map f ((x1:xs) ++ y)
  = map f (x1 : (xs ++ y))            -- по определению ++
  = f x1 : map f (xs ++ y)            -- по определению map
  = f x1 : (map f xs ++ map f y)      -- inductive hypothesis
  = (f x1 : map f xs) ++ map f y      -- по определению ++
  = map f (x1:xs) ++ map f y          -- по определению map
  = map f x ++ map f y                -- по определению x
-- Верно, что и требовалось доказать.


Теперь с этим докажем уравнения 1, 2 и 3.

Уравнение 1:

map (. g)  =  map f . map g


Воспользуемся индукцией по неявному аргументу-списку с обеих сторон, а также определением map:

-- базовый случай: пустой список
map (. g) [] = []
(map f . map g) [] = map f (map g []) = map f [] = []
-- OK
 
-- индукция: непустой список:
map (. g) (x:xs) 
  = ((. g) x) : (map (. g) xs)        -- по определению map
  = ((g x)) : (map (. g) xs)          -- по определению (.)
(map f . map g) (x:xs) 
  = map f (map g (x:xs))                  -- по определению (.)
  = map f ((g x) : (map g xs))            -- по определению map
  = ((g x)) : (map f (map g xs))        -- по определению map
  = ((g x)) : ((map f . map g) xs)      -- по определению (.)
  = ((g x)) : (map (. g) xs)          -- inductive hypothesis
-- Верно, что и требовалось доказать.


Уравнение 2:

map f . concat =  concat . map (map f)


Докажем по индукции:

-- базовый случай: пустой список
(map f . concat) [] = map f (concat []) = map f [] = []
(concat . map (map f)) [] = concat (map (map f) []) = concat [] = []
-- OK
 
-- индукция: непустой список
(map f . concat) (x:xs)
  = map f (concat (x:xs))                   -- по определению (.)
  = map f (++ concat xs)                  -- по уравнению 4 
  = map f x ++ (map f (concat xs))          -- по уравнению 6
  = map f x ++ ((map f . concat) xs)        -- по определению (.)
  = map f x ++ ((concat . map (map f)) xs)  -- inductive hypothesis
  = map f x ++ concat (map (map f) xs)      -- по определению (.)
 
(concat . map (map f)) (x:xs)
  = concat (map (map f) (x:xs))             -- по определению (.)
  = concat (map f x : map (map f) xs)       -- по определению map
  = map f x ++ concat (map (map f) xs)      -- по уравнению 4
-- Верно, что и требовалось доказать.


Уравнение 3:

concat . concat  =  concat . map concat


Как всегда, воспользуемся индукцией:

-- базовый случай: пустой список
(concat . concat) [] = concat (concat []) = concat [] = []
(concat . map concat) [] = concat (map concat []) = concat [] = []
-- Верно
 
-- индукция: непустой список
(concat . concat) (x:xs)
  = concat (concat (x:xs))                 -- по определению (.)
  = concat (++ concat xs)                -- по уравнению 4
  = concat x ++ concat (concat xs)         -- по уравнению 5
 
(concat . map concat) (x:xs)
  = concat (map concat (x:xs))             -- по определению (.)
  = concat (concat x : map concat xs)      -- по определению map
  = concat x ++ concat (map concat xs)     -- по уравнению 4
  = concat x ++ (concat . map concat) xs   -- по определению (.)
  = concat x ++ (concat . concat) xs       -- inductive hypothesis
  = concat x ++ concat (concat xs)         -- по определению (.)
-- Верно, что и требовалось доказать.



Я надеюсь, теперь у вас нет сомнений, что монада списка по-настоящему монада. ;-)

И самый интересный вопрос здесь, конечно, такой: а что мы можем сделать такого с монадой-списком, что было бы сложно без монады? Вот вам простой пример: найти все пары чисел между 1 и 6, чья сумма равняется 7 (числа — это, например, игральные кости). С помощью монады списка решить задачу элементарно:

-- Используем <font color=blue>do</font>-нотацию:
do n1 <- [1..6]
   n2 <- [1..6]
   if n1 + n2 == 7 then return (n1, n2) else []
-- Результат: [(1,6),(2,5),(3,4),(4,3),(5,2),(6,1)]


А еще можно переписать без do-нотации, только получится непонятно:

[1..6] >>= \n1 ->
  [1..6] >>= \n2 ->
    if n1 + n2 == 7 then return (n1, n2) else []


Как это работает? Вам стоило бы самим сесть и проследить все вычисления, связанные с >>= и return для списков, но вот объяснение на пальцах. Итак: [1..6] — это монадическое значение в монаде списка, и n1 пробегает всех их за раз. n2 — точно также. И возвращаются все пары (n1, n2), чья сумма корректна. Вот так мы вычисляем функцию над всеми элементами, как если бы они были одним элементом. В этом суть монады списка.

Если вы значительно поднаторели в программировании на Haskell, у вас в голове, наверно, завыла сирена. «Как же так!» — слышу я ваше возмущение. «А почему бы просто не воспользоваться генераторами списков (list comprehensions)?» И действительно:

[(n1, n2) | n1 <- [1..6], n2 <- [1..6], n1 + n2 == 7]


Возможности монады списка и генераторов списка идентичны. Выбор того или иного синтаксиса зависит от предпочтений, а также он может определяться задачей. В своей статье «Comprehending Monads» Phil Walder (в названии есть игра слов, как и во многих его статьях) даже предлагал распространить синтаксис генераторов списков на произвольные монады. Это предложение было все-таки отклонено в пользу текущей записи.

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

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


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

Содержание

Часть 1: основы
Часть 2: функции >>= и return
Часть 3: Монадные Законы
Часть 4: Монада Maybe и монада списка
  • +18
  • 7,8k
  • 6
Поделиться публикацией
Реклама помогает поддерживать и развивать наши сервисы

Подробнее
Реклама
Комментарии 6
  • +2
    Монада списка реально взрывает мозг, предпочитаю работать со списками как со списками.

    А Maybe то же самое что None в питоне. Только идеологически правильное.
    • +2
      В начале изучения действительно вводило в ступор что список это монада.

      Потом только разобрался что список это всего лишь список. А его инстанс класса Monad живёт сам по себе, можно о нём ничего не знать.
      • +1
        В начале изучения вообще не стоит упоминать это слово, а то оно только пугает. Проще принять логику Haskell в работе с самыми нужными элементами: списками, IO, Maybe, do-нотацией, — а потом уже осознание само придет, что это все монады, и ничего страшного в них нет.

        Ну, я тоже со списками работаю как со списками, хотя list comprehensions иногда очень удобны.
    • +2
      Хороший, годный торт. С нетерпением ждем следующих кусков перевода.
      • 0
        Супер! Спасибо большое за перевод.

        Мне вот интересно, а когда haskell-программисты создают свои монады (часто ли они это делают?) они реально берут ручку с бумажкой и доказывают монадические законы или?
        • +2
          У меня в этом опыта пока мало, но обычно если монада не слишком заумная, из ее вида очевидно, что законам она удовлетворяет. Но скорее всего, прежде чем ее представить общественности, программист обязательно все проверит. :)

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