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

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

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

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

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

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снова чисто Мы определяем параметризованный тип данных type 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

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

"Impurification"

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

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) worldX  =  let (resF, worldY) = f worldX 
                               in impurify resF worldY
                            =  let (resF, worldY) = f worldX      
                               in (resF, worldY)
                            =  f worldX

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

   Оставил как упражнение.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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