Почему побочные эффекты смоделированы как монады в Haskell? - PullRequest
164 голосов
/ 21 марта 2010

Кто-нибудь может дать несколько советов о том, почему нечистые вычисления в Хаскеле моделируются как монады?

Я имею в виду, что монада - это просто интерфейс с 4 операциями, так что было причиной для моделирования побочных эффектов в ней?

Ответы [ 8 ]

284 голосов
/ 22 марта 2010

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

Так что для нечистой функции

f' :: Int -> Int

мы добавляем RealWorld к рассмотрению

f :: Int -> RealWorld -> (Int, RealWorld)
-- input some states of the whole world,
-- modify the whole world because of the side effects,
-- then return the new world.

тогда f снова чист. Мы определяем параметризованный тип данных IO a = RealWorld -> (a, RealWorld), поэтому нам не нужно много раз набирать RealWorld

f :: Int -> IO Int

Для программиста непосредственная обработка RealWorld слишком опасна - в частности, если программист получает в руки значение типа RealWorld, он может попытаться скопировать его, что в принципе невозможно. (Подумайте, например, о попытке скопировать всю файловую систему. Где бы вы ее разместили?) Поэтому наше определение IO также включает в себя состояния всего мира.

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

getLine :: IO String               = RealWorld -> (String, RealWorld)
getContents :: String -> IO String = String -> RealWorld -> (String, RealWorld)
putStrLn :: String -> IO ()        = String -> RealWorld -> ((), RealWorld)

Мы хотим получить имя файла из консоли, прочитать этот файл, а затем распечатать содержимое. Как мы это сделаем, если сможем получить доступ к реальным состояниям мира?

printFile :: RealWorld -> ((), RealWorld)
printFile world0 = let (filename, world1) = getLine world0
                       (contents, world2) = (getContents filename) world1 
                   in  (putStrLn contents) world2 -- results in ((), world3)

Здесь мы видим шаблон: функции вызываются так:

...
(<result-of-f>, worldY) = f worldX
(<result-of-g>, worldZ) = g <result-of-f> worldY
...

Таким образом, мы могли бы определить оператор ~~~, чтобы связать их:

(~~~) :: (IO b) -> (b -> IO c) -> IO c

(~~~) ::      (RealWorld -> (b, RealWorld))
      -> (b -> RealWorld -> (c, RealWorld))
      ->       RealWorld -> (c, RealWorld)
(f ~~~ g) worldX = let (resF, worldY) = f worldX in
                        g resF worldY

тогда мы могли бы просто написать

printFile = getLine ~~~ getContents ~~~ putStrLn

не касаясь реального мира.


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

upperCase :: String -> String

Но чтобы попасть в реальный мир, он должен вернуть IO String. Такую функцию легко поднять:

impureUpperCase :: String -> RealWorld -> (String, RealWorld)
impureUpperCase str world = (upperCase str, world)

это можно обобщить:

impurify :: a -> IO a

impurify :: a -> RealWorld -> (a, RealWorld)
impurify a world = (a, world)

так что impureUpperCase = impurify . upperCase, а мы можем написать

printUpperCaseFile = 
    getLine ~~~ getContents ~~~ (impurify . upperCase) ~~~ putStrLn

(Примечание: обычно мы пишем getLine ~~~ getContents ~~~ (putStrLn . upperCase))


Теперь посмотрим, что мы сделали:

  1. Мы определили оператор (~~~) :: IO b -> (b -> IO c) -> IO c, который объединяет две нечистые функции вместе
  2. Мы определили функцию impurify :: a -> IO a, которая преобразует чистое значение в нечистое.

Теперь мы делаем идентификацию (>>=) = (~~~) и return = impurify, и видите? У нас есть монада.


(Чтобы проверить, действительно ли это монада, нужно выполнить несколько аксиом:

(1) return a >>= f = f a

  impurify a               = (\world -> (a, world))
 (impurify a ~~~ f) worldX = let (resF, worldY) = (\world -> (a, world)) worldX 
                             in f resF worldY
                           = let (resF, worldY) =            (a, worldX))       
                             in f resF worldY
                           = f a worldX

(2) f >>= return = f

  (f ~~~ impurify) a worldX = let (resF, worldY) = impuify a worldX 
                              in f resF worldY
                            = let (resF, worldY) = (a, worldX)     
                              in f resF worldY
                            = f a worldX

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

Упражнение.)

43 голосов
/ 16 августа 2011

Может ли кто-нибудь дать несколько советов о том, почему нечистые вычисления в Хаскеле моделируются как монады?

Этот вопрос содержит широко распространенное недоразумение. Примесь и Монада являются независимыми понятиями. Примесь не смоделирована Монадой. Скорее, есть несколько типов данных, таких как IO, которые представляют собой обязательные вычисления. И для некоторых из этих типов крошечная доля их интерфейса соответствует шаблону интерфейса, называемому «Monad». Более того, нет никакого известного чисто / функционального / денотативного объяснения IO (и вряд ли оно будет одним, учитывая цель sin bin IO), хотя обычно говорят история о World -> (a, World) значении IO a. Эта история не может правдиво описать IO, потому что IO поддерживает параллелизм и недетерминизм. Эта история даже не работает, когда речь идет о детерминированных вычислениях, которые позволяют взаимодействовать с миром в середине вычислений.

Подробнее об этом см. этот ответ .

Редактировать : Перечитывая вопрос, я не думаю, что мой ответ идет в ногу. Модели императивных вычислений часто оказываются монадами, как сказал вопрос. Запрашивающий может и не предполагать, что монадность каким-либо образом позволяет моделировать императивные вычисления.

13 голосов
/ 22 марта 2010

Насколько я понимаю, кто-то по имени Eugenio Moggi впервые заметил, что ранее неизвестная математическая конструкция, называемая "монадой", может использоваться для моделирования побочных эффектов в компьютерных языках и, следовательно, для определения их семантики с использованием лямбда-исчисления.,Когда Haskell разрабатывался, были различные способы, которыми были смоделированы нечистые вычисления (см. Бумагу «рубашка для волос» Саймона Пейтона Джонса для более подробной информации), но когда Фил Уодлер представил монады, быстро стало очевидно, что это былоОтвет.А остальное уже история.

8 голосов
/ 22 марта 2010

Может ли кто-нибудь дать несколько советов о том, почему нечистые вычисления в Хаскеле моделируются как монады?

Ну, потому что Haskell чист . Вам нужна математическая концепция, чтобы различать не чистые вычисления и чистые на уровне типа и моделировать программные потоки соответственно.

Это означает, что вам нужно будет получить какой-то тип IO a, который моделирует неочищенные вычисления. Тогда вам нужно знать, как объединить , эти вычисления, из которых применяются в последовательности (>>=) и поднять значение (return), являются наиболее очевидные и основные.

С этими двумя вы уже определили монаду (даже не думая об этом);)

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

См. монады в функциональном программировании и уникальность ввода (единственная известная мне альтернатива) для получения дополнительной информации.

6 голосов
/ 30 сентября 2014

Как вы говорите, Monad - это очень простая структура.Половина ответа такова: Monad - это самая простая структура, которую мы могли бы дать побочным функциям и использовать их.С Monad мы можем сделать две вещи: мы можем рассматривать чистое значение как значение с побочными эффектами (return), и мы можем применить функцию с побочными эффектами к значению с побочными эффектами, чтобы получить новый побочный эффектзначение (>>=).Потеря способности делать что-либо из перечисленного может нанести вред, поэтому наш тип побочных эффектов должен быть «по крайней мере» Monad, и оказывается, что Monad достаточно для реализации всего, что нам нужно до сих пор.

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

Хорошо, что мы можем сказать об этой операции?Это ассоциативно;то есть, если мы объединяем три побочных эффекта, не имеет значения, в каком порядке мы выполняем объединение. Если мы делаем (запись файла, затем чтение сокета), затем выключаем компьютер, это то же самое, что делать запись файла тогда (чтение сокета, затем выключениекомпьютер).Но это не коммутативно: («запись файла» и «удаление файла») - это другой побочный эффект («удаление файла» и «запись файла»).И у нас есть идентичность: специальный побочный эффект «без побочных эффектов» работает («без побочных эффектов», тогда «удаление файла» - это тот же побочный эффект, что и «удаление файла»). В этот момент любой математик думает «Группа!»Но у групп есть обратное, и нет никакого способа обратить побочный эффект вообще;«Удалить файл» необратим.Таким образом, структура, которую мы оставили, является структурой моноида, что означает, что наши побочные функции должны быть монадами.

Есть ли более сложная структура?Конечно!Мы могли бы разделить возможные побочные эффекты на эффекты файловой системы, сетевые эффекты и многое другое, и мы могли бы придумать более сложные правила композиции, которые сохранили бы эти детали.Но опять-таки все сводится к следующему: Monad очень прост, но все же достаточно мощный, чтобы выразить большинство свойств, которые нас интересуют.(В частности, ассоциативность и другие аксиомы позволяют нам тестировать наше приложение на небольших кусочках, с уверенностью, что побочные эффекты комбинированного приложения будут такими же, как комбинация побочных эффектов кусочков).

4 голосов
/ 22 марта 2010

На самом деле это довольно чистый способ функционального подхода к вводу / выводу.

В большинстве языков программирования вы выполняете операции ввода / вывода.В Haskell представьте, что вы пишете код не для выполнения операций, а для генерации списка операций, которые вы хотели бы сделать.

Монады - это просто красивый синтаксис именно для этого.

Если вы хотите знать, почему монады, а не что-то другое, я думаю, ответ заключается в том, что это лучший функциональный способ представления ввода / вывода, о котором люди могли подумать, когда создавали Haskell.

3 голосов
/ 22 марта 2010

AFAIK, причина в том, чтобы иметь возможность включать проверку побочных эффектов в системе типов. Если вы хотите узнать больше, послушайте эти SE-Radio эпизоды: Эпизод 108: Саймон Пейтон Джонс о функциональном программировании и Haskell Эпизод 72: Эрик Мейер на LINQ

2 голосов
/ 07 января 2012

Выше приведены очень хорошие подробные ответы с теоретическим обоснованием.Но я хочу высказать свое мнение о монаде IO.Я не опытный программист на Haskell, так что, может быть, это довольно наивно или даже неправильно.Но я помог мне в некоторой степени разобраться с монадой ввода-вывода (обратите внимание, что она не относится к другим монадам).

Сначала я хочу сказать, что пример с «реальным миром» мне не слишком понятенпоскольку мы не можем получить доступ к его (реальному миру) предыдущим состояниям.Может быть, это совсем не относится к вычислениям монад, но желательно в смысле ссылочной прозрачности, которая обычно присутствует в коде haskell.

Поэтому мы хотим, чтобы наш язык (haskell) был чистым.Но нам нужны операции ввода / вывода, так как без них наша программа не может быть полезной.И эти операции не могут быть чистыми по своей природе.Таким образом, единственный способ справиться с этим - отделить нечистые операции от остальной части кода.

Здесь появляется монада.На самом деле, я не уверен, что не может быть другой конструкции с аналогичными необходимыми свойствами, но дело в том, что у монады есть эти свойства, поэтому ее можно использовать (и она успешно используется).Основным свойством является то, что мы не можем избежать этого.В интерфейсе монады нет операций, позволяющих избавиться от монады вокруг нашего значения.Другие (не IO) монады предоставляют такие операции и допускают сопоставление с образцом (например, Maybe), но эти операции не находятся в интерфейсе монады.Другим обязательным свойством является возможность цепочки операций.

Если мы думаем о том, что нам нужно с точки зрения системы типов, мы приходим к тому, что нам нужен тип с конструктором, который можно обернуть вокруг любой переменной.Конструктор должен быть закрытым, поскольку мы запрещаем выходить из него (т. Е. Сопоставление с образцом).Но нам нужна функция для помещения значения в этот конструктор (здесь на ум приходит return).И нам нужен способ цепочки операций.Если мы подумаем об этом в течение некоторого времени, мы придем к тому, что операция сцепления должна иметь тип как >> = has.Итак, мы приходим к чему-то очень похожему на монаду.Я думаю, что если мы сейчас проанализируем возможные противоречивые ситуации с этой конструкцией, мы придем к аксиомам монад.

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

Теперь некоторый набор нечистых операций предопределенязык в этой выбранной монаде IO.Мы можем объединить эти операции для создания новых неочищенных операций.И все эти операции должны иметь IO в своем типе.Однако обратите внимание, что присутствие IO в типе некоторой функции не делает эту функцию нечистой.Но, как я понимаю, писать чистые функции с IO по своему типу - плохая идея, так как изначально наша идея заключалась в разделении чистых и нечистых функций.

Наконец, я хочу сказать, что монада не превращаетсянечистые операции в чистые.Это позволяет только эффективно разделить их.(Повторяю, это только мое понимание)

...