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

Question

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

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

Answer 1

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

Таким образом, для нечистой функции

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))}

---

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

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

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

Answer 2

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

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

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

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

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

Для получения дополнительной информации см. monads in functional programming и uniqueness typing (единственная альтернатива, которую я знаю).

Answer 3

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

Answer 4

Как я понимаю, кто-то назвал Eugenio Moggi первым заметил, что ранее неясными математическая конструкция называется «Монада» может быть использован для моделирования побочных эффектов в компьютерных языках, и, следовательно, определить их семантику с помощью лямбда-исчисления , Когда разрабатывался Haskell, были разные способы моделирования нечистых вычислений (см. Simon Peyton Jones '"hair shirt" paper), но когда Фил Вадлер представил монады, стало очевидно, что это был «Ответ». И остальное уже история.

Answer 5

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

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

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

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

Answer 6

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

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

Дополнительное разъяснение см. В this answer.

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

Answer 7

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

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

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

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

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

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

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

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

Answer 8

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

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

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

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