Почему побочные эффекты смоделированы как монады в Haskell?
Кто-нибудь может дать несколько советов о том, почему нечистые вычисления в Хаскеле моделируются как монады?
Я имею в виду, что монада - это просто интерфейс с 4 операциями, так что же было причиной для моделирования побочных эффектов в ней?
8 ответов
Предположим, что функция имеет побочные эффекты. Если мы возьмем все эффекты, которые он производит, в качестве входных и выходных параметров, то функция будет чистой для внешнего мира.
Так что для нечистой функции
f' :: Int -> Int
мы добавляем RealWorld к рассмотрению
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 слишком опасна - в частности, если программист получает в свои руки значение типа 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) )
Теперь посмотрим, что мы сделали:
- Мы определили оператор
(~~~) :: 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
Упражнение.)
Может ли кто-нибудь дать несколько советов о том, почему нечистые вычисления в Хаскеле моделируются как монады?
Этот вопрос содержит широко распространенное недоразумение. Примесь и Монада являются независимыми понятиями. Примесь не моделируется Монадой. Скорее, есть несколько типов данных, таких как IO, которые представляют собой императивный расчет. И для некоторых из этих типов крошечная доля их интерфейса соответствует шаблону интерфейса, названному "Монадой". Более того, нет никакого известного чисто / функционального / дентивативного объяснения IO (и вряд ли будет один, учитывая цель "бин бин" IO), хотя есть обычно рассказанная история о World -> (a, World) быть смыслом IO a, Эта история не может правдиво описать IO, так как IO поддерживает параллелизм и недетерминизм. История даже не работает, когда для детерминированных вычислений, которые позволяют взаимодействию в середине вычислений с миром.
Для более подробного объяснения см. Этот ответ.
Изменить: Перечитывая вопрос, я не думаю, что мой ответ идет в правильном направлении. Модели императивных вычислений часто оказываются монадами, как и сказал вопрос. Запрашивающий может и не предполагать, что монадность каким-либо образом позволяет моделировать императивные вычисления.
Насколько я понимаю, кто-то по имени Эудженио Могги впервые заметил, что ранее неизвестная математическая конструкция, называемая "монадой", могла использоваться для моделирования побочных эффектов в компьютерных языках и, следовательно, для определения их семантики с использованием лямбда-исчисления. Когда разрабатывался Haskell, существовали различные способы моделирования нечистых вычислений (см. Статью Саймона Пейтона Джонса "Волшебная рубашка" для более подробной информации), но когда Фил Уодлер представил монады, быстро стало очевидно, что это был "Ответ". И остальное уже история.
Может ли кто-нибудь дать несколько советов о том, почему нечистые вычисления в Хаскеле моделируются как монады?
Ну, потому что Хаскелл чист. Вам нужна математическая концепция, чтобы различать неочищенные и чистые вычисления на уровне типов и моделировать потоки программ соответственно.
Это означает, что вам придется в конечном итоге с какой-то тип IO a это моделирует нечистое вычисление. Тогда вам нужно знать способы объединения этих вычислений, которые применяются последовательно (>>=) и поднять значение (return) являются наиболее очевидными и основными.
С этими двумя вы уже определили монаду (даже не думая об этом);)
Кроме того, монады предоставляют очень общие и мощные абстракции, поэтому многие виды потока управления можно удобно обобщать в монадических функциях, таких как sequence, liftM или особый синтаксис, делающий нечистоту не таким особенным случаем.
См. Монады в функциональном программировании и уникальной типизации (единственная альтернатива, которую я знаю) для получения дополнительной информации.
Как ты говоришь, Monad это очень простая структура. Одна половина ответа: Monad это самая простая структура, которую мы могли бы дать побочным функциям и использовать их. С Monad мы можем сделать две вещи: мы можем рассматривать чистое значение как побочное значение (return), и мы можем применить побочную функцию к побочному значению, чтобы получить новое побочное значение (>>=). Потеря способности делать что-либо из этого может нанести вред, поэтому наш побочный тип должен быть "как минимум" Monadи получается Monad достаточно, чтобы реализовать все, что нам нужно до сих пор.
Другая половина: какую самую детальную структуру мы могли бы дать "возможным побочным эффектам"? Мы можем, конечно, думать о пространстве всех возможных побочных эффектов как о множестве (единственная операция, которая требует членства). Мы можем объединить два побочных эффекта, выполняя их один за другим, и это приведет к другому побочному эффекту (или, возможно, к одному и тому же - если первым был "компьютер выключения", а вторым "запись файла", то результат сочинение это просто "выключение компьютера").
Итак, что мы можем сказать об этой операции? Это ассоциативно; то есть, если мы объединяем три побочных эффекта, не имеет значения, в каком порядке мы выполняем объединение. Если мы делаем (запись файла, затем чтение сокета), затем выключаем компьютер, это то же самое, что делать запись файла тогда (чтение сокета, затем выключение компьютер). Но это не коммутативно: ("запись файла", затем "удаление файла") - это другой побочный эффект от ("удаление файла" и "запись файла"). И у нас есть идентичность: специальный побочный эффект "без побочных эффектов" работает ("без побочных эффектов", тогда "удалить файл" - это тот же побочный эффект, что и "удалить файл"). В этот момент любой математик думает "Группа!" Но у групп есть обратное, и нет никакого способа обратить побочный эффект вообще; "Удалить файл" необратим. Таким образом, структура, которую мы оставили, является структурой моноида, что означает, что наши побочные функции должны быть монадами.
Есть ли более сложная структура? Конечно! Мы могли бы разделить возможные побочные эффекты на эффекты файловой системы, сетевые эффекты и многое другое, и мы могли бы придумать более сложные правила композиции, которые сохранили бы эти детали. Но снова это сводится к: Monad очень прост, и все же достаточно мощный, чтобы выразить большинство свойств, которые нас интересуют. (В частности, ассоциативность и другие аксиомы позволяют нам тестировать наше приложение на маленьких кусочках, с уверенностью, что побочные эффекты комбинированного приложения будут такими же, как комбинация побочных эффектов кусочков).
На самом деле это довольно чистый способ думать о вводе / выводе функционально.
В большинстве языков программирования вы выполняете операции ввода / вывода. В Haskell представьте, что вы пишете код не для выполнения операций, а для генерации списка операций, которые вы хотели бы выполнить.
Монады - просто красивый синтаксис именно для этого.
Если вы хотите знать, почему монады, а не что-то другое, я думаю, что ответ заключается в том, что это лучший функциональный способ представления ввода / вывода, о котором люди могли подумать, когда делали Haskell.
AFAIK, причина в том, чтобы иметь возможность включить проверку побочных эффектов в систему типов. Если вы хотите узнать больше, послушайте эти эпизоды SE-Radio: Эпизод 108: Саймон Пейтон Джонс о функциональном программировании и Эскод 72 Хаскелла: Эрик Мейер в LINQ
Выше очень хорошие подробные ответы с теоретическим обоснованием. Но я хочу высказать свое мнение о монаде IO. Я не опытный программист на Haskell, так что, может быть, это довольно наивно или даже неправильно. Но я помог мне разобраться с IO-монадой в некоторой степени (обратите внимание, что она не относится к другим монадам).
Во-первых, я хочу сказать, что пример с "реальным миром" для меня не слишком понятен, так как мы не можем получить доступ к его (реальному миру) предыдущим состояниям. Может быть, это вообще не относится к вычислениям монад, но желательно в смысле ссылочной прозрачности, которая обычно представлена в коде haskell.
Поэтому мы хотим, чтобы наш язык (haskell) был чистым. Но нам нужны операции ввода / вывода, так как без них наша программа не может быть полезной. И эти операции не могут быть чистыми по своей природе. Таким образом, единственный способ справиться с этим - отделить нечистые операции от остальной части кода.
Здесь приходит монада. На самом деле, я не уверен, что не может быть другой конструкции с аналогичными необходимыми свойствами, но дело в том, что у монады есть эти свойства, поэтому ее можно использовать (и она успешно используется). Основным свойством является то, что мы не можем избежать этого. В интерфейсе монады нет операций, позволяющих избавиться от монады вокруг нашего значения. Другие (не IO) монады предоставляют такие операции и допускают сопоставление с образцом (например, Maybe), но эти операции не находятся в интерфейсе монады. Другим обязательным свойством является способность связывать операции.
Если мы думаем о том, что нам нужно с точки зрения системы типов, мы приходим к тому, что нам нужен тип с конструктором, который можно обернуть вокруг любой переменной. Конструктор должен быть закрытым, поскольку мы запрещаем выходить из него (т. Е. Сопоставление с образцом). Но нам нужна функция, чтобы поместить значение в этот конструктор (здесь приходит на ум возвращение). И нам нужен способ цепочки операций. Если мы подумаем об этом в течение некоторого времени, мы придем к тому, что операция сцепления должна иметь тип как >>= has. Итак, мы приходим к чему-то очень похожему на монаду. Я думаю, что если мы сейчас проанализируем возможные противоречивые ситуации с этой конструкцией, мы придем к аксиомам монады.
Обратите внимание, что разработанная конструкция не имеет ничего общего с примесями. У него есть только те свойства, которые мы хотели бы иметь, чтобы иметь возможность иметь дело с нечистыми операциями, а именно: отсутствие выхода, сцепление и способ входа.
Теперь некоторый набор нечистых операций предопределен языком в этой выбранной монаде IO. Мы можем объединить эти операции для создания новых неочищенных операций. И все эти операции должны иметь IO в своем типе. Однако обратите внимание, что присутствие IO в типе некоторой функции не делает эту функцию нечистой. Но, как я понимаю, писать чистые функции с IO по своему типу - плохая идея, так как изначально мы хотели разделить чистые и нечистые функции.
Наконец, я хочу сказать, что монада не превращает нечистые операции в чистые. Это позволяет только эффективно разделить их. (Повторюсь, это только мое понимание)