Почему побочные эффекты моделируются как монады в Haskell?

Question

Почему побочные эффекты моделируются как монады в Haskell?

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

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

728 8

haskell functional-programming monads

8 ответов:

Comments

Ничего не найдено.

kennytm · Accepted Answer · 2016-10-01 16:47:37

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

так для нечистой функции
f' :: Int -> Int
мы добавляем реальный мир к рассмотрению
f :: Int -> RealWorld -> (Int, RealWorld)
-- input some states of the whole world,
-- modify the whole world because of the a side effects,
-- then return the new world.
затем f опять чисто. Мы определяем параметризованный тип данных IO a = RealWorld -> (a, RealWorld), так что нам не нужно вводить RealWorld так много раз
f :: Int -> IO Int
для программиста, обработка реального мира напрямую слишком опасна-в частности, если программист получает в свои руки значение типа RealWorld, они могут попытаться скопировать это, что в принципе невозможно. (Например, попробуйте скопировать всю файловую систему. Куда бы вы его положили?) Поэтому наше определение ИО инкапсулирует состояния всего мира.

эти нечистые функции бесполезны, если мы не можем связать их вместе. Считать
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))}

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

мы определили оператор (~~~) :: IO b -> (b -> IO c) -> IO c который связывает две нечистые функции вместе

мы определили функцию 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

физические упражнения.)

Conal · Accepted Answer · 2017-05-23 15:34:30

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

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

для более подробного объяснения, см. ответ.

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

Paul Johnson · Accepted Answer · 2010-03-22 09:54:22

Как я понимаю, кто-то назвал Эухенио Моджи впервые заметил, что ранее неясная математическая конструкция, называемая "монадой", может использоваться для моделирования побочных эффектов в компьютерных языках и, следовательно, определять их семантику с помощью лямбда-исчисления. Когда Хаскелл разрабатывался, существовали различные способы моделирования нечистых вычислений (см. Саймон Пейтон Джонс "власяницу" бумага для более подробной информации), но когда Фил Уодлер представил монады это быстро стало очевидно, что это и есть ответ. А остальное-уже история.

Dario · Accepted Answer · 2010-03-21 23:24:41

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

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

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

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

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

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

lmm · Accepted Answer · 2014-09-30 04:08:46

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

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

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

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

Noah Lavine · Accepted Answer · 2010-03-22 16:44:03

Это на самом деле довольно чистый способ думать ввода в функциональном стиле.

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

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

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

Gabriel Ščerbák · Accepted Answer · 2010-04-08 11:14:47

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

Dmitrii Semikin · Accepted Answer · 2012-01-06 22:12:08

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

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

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

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

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

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

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