Почему побочные эффекты в Haskell моделируются как монады?
https://stackoverflow.com/questions/2488646
-
21-09-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianВопрос
Может ли кто-нибудь подсказать, почему нечистые вычисления в Haskell моделируются как монады?
Я имею в виду, что монада — это просто интерфейс с четырьмя операциями, так что же послужило причиной моделирования в нем побочных эффектов?
Решение
Предположим, что функция имеет побочные эффекты.Если мы возьмем все эффекты, которые она производит, в качестве входных и выходных параметров, то функция будет чистой для внешнего мира.
Итак, для нечистой функции
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))
Теперь посмотрим, что мы сделали:
- Мы определили оператор
(~~~) :: 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
Упражнение.)
Другие советы
Может ли кто-нибудь подсказать, почему нечистые вычисления в Haskell моделируются как монады?
Этот вопрос содержит широко распространенное недоразумение.Примесь и Монада — независимые понятия.Примеси нет смоделировано Монадой.Скорее, существует несколько типов данных, таких как IO, которые представляют собой императивные вычисления.И для некоторых из этих типов крошечная часть интерфейса соответствует шаблону интерфейса, называемому «Монада».Более того, не существует известного чистого/функционального/денотативного объяснения IO (и вряд ли он будет, учитывая "корзина для грехов" Цель IO), хотя существует широко распространенная история о World -> (a, World) смысл IO a.Эта история не может правдиво описать IO, потому что IO поддерживает параллелизм и недетерминизм.Эта история не работает даже для детерминированных вычислений, которые позволяют взаимодействовать с миром в середине вычислений.
Дополнительные пояснения см. этот ответ.
Редактировать:Перечитывая вопрос, я не думаю, что мой ответ совсем правильный.Модели императивных вычислений часто оказываются монадами, как и было сказано в вопросе.Задающий вопрос может на самом деле не предполагать, что монадность каким-либо образом позволяет моделировать императивные вычисления.
Я так понимаю, кто-то звонил Эухенио Моджи впервые заметил, что ранее неясная математическая конструкция под названием «монада» может использоваться для моделирования побочных эффектов в компьютерных языках и, следовательно, для определения их семантики с помощью лямбда-исчисления.Когда разрабатывался Haskell, существовали различные способы моделирования нечистых вычислений (см. работу Саймона Пейтона Джонса). бумага «власяница» подробнее), но когда Фил Уодлер представил монады, быстро стало очевидно, что это и есть Ответ.И остальное уже история.
Может ли кто-нибудь подсказать, почему нечистые вычисления в Haskell моделируются как монады?
Ну, потому что Хаскель чистый.Вам нужна математическая концепция, чтобы различать нечистые вычисления и чистые на уровень типа и моделировать программные потоки в соответственно.
Это означает, что вам придется получить какой-то тип IO a который моделирует нечистые вычисления.Тогда вам нужно знать способы объединение эти вычисления, из которых применять последовательно (>>=) и поднять ценность (return) являются наиболее очевидными и основными.
С помощью этих двух вы уже определили монаду. (даже не задумываясь об этом);)
Кроме того, монады обеспечивают очень общие и мощные абстракции, поэтому многие виды потока управления можно удобно обобщить в монадических функциях, таких как sequence, liftM или специальный синтаксис, что делает нечистоту не таким уж особым случаем.
Видеть монады в функциональном программировании и уникальность типизации (единственная известная мне альтернатива) для получения дополнительной информации.
Как ты говоришь, Monad представляет собой очень простую структуру.Половина ответа: Monad — это простейшая структура, которую мы могли бы придать функциям с побочными эффектами и иметь возможность их использовать.С Monad мы можем сделать две вещи:мы можем рассматривать чистое значение как значение, оказывающее побочный эффект (return), и мы можем применить функцию побочного эффекта к побочному значению, чтобы получить новое побочное значение (>>=).Потеря способности делать любую из этих вещей была бы парализующей, поэтому наш тип побочных эффектов должен быть «по крайней мере» Monad, и оказывается Monad достаточно, чтобы реализовать все, что нам нужно до сих пор.
Другая половина:Какую наиболее подробную структуру мы могли бы дать «возможным побочным эффектам»?Мы, конечно, можем рассматривать пространство всех возможных побочных эффектов как набор (единственная операция, которая требует этого, — это членство).Мы можем объединить два побочных эффекта, выполняя их один за другим, и это приведет к другому побочному эффекту (или, возможно, одному и тому же — если первый был «выключение компьютера», а второй — «запись файла», то результат их составление — это просто «выключение компьютера»).
Хорошо, что можно сказать об этой операции?Это ассоциативно;то есть, если мы объединим три побочных эффекта, не имеет значения, в каком порядке мы будем это объединять.Если мы это сделаем (запись файла, затем чтение сокета), а затем выключение компьютера, это то же самое, что и запись файла затем (чтение сокета, затем выключение компьютера).Но это не коммутативно:(«записать файл», затем «удалить файл») — это побочный эффект, отличный от («удалить файл», затем «записать файл»).И у нас есть личность:Специальный побочный эффект «Нет побочных эффектов» работает («без побочных эффектов», тогда «удалить файл» - это тот же побочный эффект, что и просто «Удалить файл»), на данный момент любой математик думает «Группа!» Но у групп есть инверсии, и нет никакого способа инвертировать побочный эффект в целом;«удалить файл» необратимо.Таким образом, у нас осталась структура моноида, а это означает, что наши побочные эффекты должны быть монадами.
Есть ли более сложная структура?Конечно!Мы могли бы разделить возможные побочные эффекты на эффекты, основанные на файловой системе, эффекты, основанные на сети и т. д., и мы могли бы придумать более сложные правила композиции, которые сохраняли бы эти детали.Но опять же дело в следующем: Monad очень простой, но достаточно мощный, чтобы выразить большинство свойств, которые нас интересуют.(В частности, ассоциативность и другие аксиомы позволяют нам тестировать наше приложение небольшими частями, с уверенностью, что побочные эффекты комбинированного приложения будут такими же, как и комбинация побочных эффектов этих частей).
На самом деле это довольно простой способ функционального подхода к вводу-выводу.
В большинстве языков программирования вы выполняете операции ввода/вывода.Представьте себе, что в Haskell вы пишете код, который не делать операций, а для создания списка операций, которые вы хотели бы выполнить.
Монады — это просто красивый синтаксис именно для этого.
Если вы хотите знать, почему монады противопоставляются чему-то еще, я думаю, ответ таков: они являются лучшим функциональным способом представления ввода-вывода, о котором люди могли подумать, когда создавали Haskell.
AFAIK, причина в том, чтобы иметь возможность включать проверки побочных эффектов в систему типов.Если вы хотите узнать больше, послушайте эти СЭ-Радио эпизоды:Эпизод 108:Саймон Пейтон Джонс о функциональном программировании и Haskell Episode 72:Эрик Мейер о LINQ
Выше есть очень хорошие подробные ответы с теоретической подготовкой.Но я хочу высказать свое мнение о монаде IO.Я не опытный программист на Haskell, так что, возможно, это довольно наивно или даже неправильно.Но мне в какой-то степени помогло разобраться с монадой IO (обратите внимание, что она не имеет отношения к другим монадам).
Прежде всего я хочу сказать, что этот пример с «реальным миром» для меня не слишком ясен, поскольку мы не можем получить доступ к его (реальному миру) предыдущим состояниям.Возможно, это вообще не относится к монадным вычислениям, но желательно в смысле ссылочной прозрачности, которая обычно присутствует в коде Haskell.
Итак, мы хотим, чтобы наш язык (хаскелл) был чистым.Но нам нужны операции ввода/вывода, без них наша программа не сможет быть полезной.И эти операции не могут быть чистыми по своей природе.Поэтому единственный способ справиться с этим — отделить нечистые операции от остального кода.
Здесь приходит монада.На самом деле, я не уверен, что не может существовать другой конструкции с аналогичными необходимыми свойствами, но дело в том, что монада обладает этими свойствами, поэтому ее можно использовать (и она успешно используется).Главное свойство состоит в том, что мы не можем от него уйти.В интерфейсе монады нет операций по избавлению от монады вокруг нашего значения.Другие (не IO) монады предоставляют такие операции и допускают сопоставление с образцом (например,Возможно), но этих операций нет в интерфейсе монады.Еще одним обязательным свойством является возможность связывать операции в цепочку.
Если задуматься о том, что нам нужно с точки зрения системы типов, то приходим к тому, что нам нужен тип с конструктором, который можно обернуть вокруг любого значения.Конструктор должен быть приватным, так как мы запрещаем выход из него (т.сопоставление с образцом).Но нам нужна функция, которая будет помещать значение в этот конструктор (здесь на ум приходит возврат).И нам нужен способ объединить операции.Если мы подумаем об этом некоторое время, то придем к тому, что операция связывания должна иметь тип, такой как >>=.Итак, мы приходим к чему-то очень похожему на монаду.Думаю, если мы теперь проанализируем возможные противоречивые ситуации с этим конструктом, мы придем к аксиомам монады.
Отметим, что разработанная конструкция не имеет ничего общего с примесью.У него есть только свойства, которые мы хотели иметь для работы с нечистыми операциями, а именно: невозможность экранирования, цепочка и способ проникновения.
Теперь некоторый набор нечистых операций предопределен языком внутри выбранной монады IO.Мы можем объединить эти операции для создания новых нечистых операций.И все эти операции должны иметь в своем типе ввод-вывод.Однако обратите внимание, что наличие ввода-вывода в типе некоторой функции не делает эту функцию нечистой.Но, насколько я понимаю, писать чистые функции с IO в их типе — плохая идея, поскольку изначально нашей идеей было разделить чистые и нечистые функции.
Напоследок хочу сказать, что монада не превращает нечистые операции в чистые.Это позволяет лишь эффективно их разделить.(повторяю, это только мое понимание)
