Dlaczego efekty uboczne są modelowane jako monady w Haskell?

Czy ktokolwiek mógłby podać kilka wskazówek, dlaczego nieczyste obliczenia w Haskell są modelowane jako monady?

Chodzi mi o to, że monada to tylko interfejs z 4 operacjami, więc jaki był powód modelowania w niej efektów ubocznych?

Załóżmy, że funkcja ma skutki uboczne. Jeśli weźmiemy wszystkie wywoływane przez nią efekty jako parametry wejściowe i wyjściowe, wówczas funkcja jest czysta dla świata zewnętrznego.

Więc dla nieczystej funkcji

f' :: Int -> Int

do rozważań dodajemy 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.

potem fznów jest czysty. Definiujemy sparametryzowany typ danych type IO a = RealWorld -> (a, RealWorld), więc nie musimy tyle razy wpisywać RealWorld i możemy po prostu pisać

f :: Int -> IO Int

Dla programisty bezpośrednia obsługa RealWorld jest zbyt niebezpieczna - w szczególności, jeśli programista zdobędzie wartość typu RealWorld, może spróbować skopiować , co jest w zasadzie niemożliwe. (Pomyśl na przykład o próbie skopiowania całego systemu plików. Gdzie byś to umieścił?) Dlatego nasza definicja IO obejmuje również stany całego świata.

Skład funkcji „nieczystych”

Te nieczyste funkcje są bezużyteczne, jeśli nie możemy ich połączyć. Rozważać

getLine     :: IO String            ~            RealWorld -> (String, RealWorld)
getContents :: String -> IO String  ~  String -> RealWorld -> (String, RealWorld)
putStrLn    :: String -> IO ()      ~  String -> RealWorld -> ((),     RealWorld)

Chcemy, aby

• pobrać nazwę pliku z konsoli,
• przeczytaj ten plik i
• wypisuje zawartość tego pliku na konsoli.

Jak byśmy to zrobili, gdybyśmy mieli dostęp do stanów świata rzeczywistego?

printFile :: RealWorld -> ((), RealWorld)
printFile world0 = let (filename, world1) = getLine world0
                       (contents, world2) = (getContents filename) world1 
                   in  (putStrLn contents) world2 -- results in ((), world3)

Widzimy tutaj wzór. Funkcje nazywane są w ten sposób:

...
(<result-of-f>, worldY) = f               worldX
(<result-of-g>, worldZ) = g <result-of-f> worldY
...

Moglibyśmy więc zdefiniować operator, ~~~aby je powiązać:

(~~~) :: (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

wtedy moglibyśmy po prostu napisać

printFile = getLine ~~~ getContents ~~~ putStrLn

bez dotykania prawdziwego świata.

„Nieczystość”

Załóżmy teraz, że chcemy, aby zawartość pliku również była wielka. Wielkie litery to czysta funkcja

upperCase :: String -> String

Ale aby trafić do prawdziwego świata, musi zwrócić plik IO String. Łatwo jest podnieść taką funkcję:

impureUpperCase :: String -> RealWorld -> (String, RealWorld)
impureUpperCase str world = (upperCase str, world)

Można to uogólnić:

impurify :: a -> IO a

impurify :: a -> RealWorld -> (a, RealWorld)
impurify a world = (a, world)

więc impureUpperCase = impurify . upperCasei możemy pisać

printUpperCaseFile = 
    getLine ~~~ getContents ~~~ (impurify . upperCase) ~~~ putStrLn

_{(Uwaga: zwykle piszemy getLine ~~~ getContents ~~~ (putStrLn . upperCase))}

Cały czas pracowaliśmy z monadami

Zobaczmy teraz, co zrobiliśmy:

1. Zdefiniowaliśmy operator, (~~~) :: IO b -> (b -> IO c) -> IO cktóry łączy ze sobą dwie nieczyste funkcje
2. Zdefiniowaliśmy funkcję, impurify :: a -> IO aktóra przekształca czystą wartość w nieczystą.

Teraz możemy sprawić, że identyfikacja (>>=) = (~~~)i return = impurify, i zobaczyć? Mamy monadę.

Uwaga techniczna

Aby upewnić się, że to naprawdę monada, wciąż jest kilka aksjomatów, które również należy sprawdzić:

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

   Pozostawiony jako ćwiczenie.

Czy ktokolwiek mógłby dać kilka wskazówek, dlaczego nieczytelne obliczenia w Haskell są modelowane jako monady?

To pytanie zawiera powszechne nieporozumienie. Nieczystość i monada to niezależne pojęcia. Nieczystość nie jest wzorowana przez Monadę. Jest raczej kilka typów danych, takich jak te IO, które reprezentują bezwzględne obliczenia. W przypadku niektórych z tych typów niewielki ułamek ich interfejsu odpowiada wzorcowi zwanemu „Monadą”. Co więcej, nie ma znanego czystego / funkcjonalnego / denotacyjnego wyjaśnienia IO(i jest mało prawdopodobne, aby takie było, biorąc pod uwagę cel „sin bin”IO ), chociaż istnieje powszechnie opowiadana historia o World -> (a, World)byciu znaczeniem IO a. Tej historii nie można zgodnie z prawdą opisać IO, ponieważIOobsługuje współbieżność i niedeterminizm. Ta historia nie działa nawet w przypadku deterministycznych obliczeń, które pozwalają na interakcję ze światem w trakcie obliczeń.

Więcej wyjaśnień znajdziesz w tej odpowiedzi .

Edycja : Po ponownym przeczytaniu pytania nie sądzę, że moja odpowiedź jest na dobrej drodze. Modele imperatywnych obliczeń często okazują się monadami, tak jak brzmiało pytanie. Pytający może tak naprawdę nie zakładać, że monadyczność w jakikolwiek sposób umożliwia modelowanie imperatywnych obliczeń.

Jak rozumiem, ktoś o nazwisku Eugenio Moggi jako pierwszy zauważył, że wcześniej niejasny konstrukt matematyczny zwany „monadą” może być użyty do modelowania skutków ubocznych w językach komputerowych, a zatem określić ich semantykę za pomocą rachunku Lambda. Kiedy opracowywano Haskell, istniały różne sposoby modelowania nieczystych obliczeń ( więcej szczegółów w artykule Simona Peytona Jonesa o „koszuli do włosów” ), ale kiedy Phil Wadler przedstawił monady, szybko stało się oczywiste, że to Odpowiedź. A reszta to historia.

Czy ktokolwiek mógłby dać kilka wskazówek, dlaczego nieczytelne obliczenia w Haskell są modelowane jako monady?

Cóż, ponieważ Haskell jest czysty . Potrzebny jest pojęcie matematyczne odróżnić unpure obliczeń i czystych te na typ poziomie i do modelu programowe płynie w odpowiednio.

Oznacza to, że będziesz musiał skończyć z pewnym typem, IO aktóry modeluje nieprecyzyjne obliczenia. Następnie musisz znać sposoby łączenia tych obliczeń, które mają zastosowanie w sekwencji ( >>=) i podnoszenie wartości ( return) są najbardziej oczywiste i podstawowe.

Z tymi dwoma już zdefiniowałeś monadę (nawet o tym nie myśląc);)

Ponadto monady zapewniają bardzo ogólne i potężne abstrakcje , więc wiele rodzajów kontroli przepływu można łatwo uogólnić w monadycznych funkcji, takich jak sequence, liftMlub specjalnej składni, dzięki czemu unpureness nie taki szczególny przypadek.

Zobacz monady w programowaniu funkcjonalnym i typowaniu unikalności (jedyna znana mi alternatywa), aby uzyskać więcej informacji.

Jak mówisz, Monadjest to bardzo prosta konstrukcja. Połowa odpowiedzi brzmi: Monadto najprostsza struktura, jaką moglibyśmy nadać funkcjom wywołującym skutki uboczne i móc z nich korzystać. Dzięki temu Monadmożemy zrobić dwie rzeczy: możemy traktować czystą wartość jako wartość powodującą efekt uboczny (return ) i możemy zastosować funkcję powodującą efekt uboczny do wartości powodującej efekt uboczny, aby uzyskać nową wartość powodującą efekt uboczny ( >>=). Utrata możliwości zrobienia którejkolwiek z tych rzeczy byłaby paraliżująca, więc nasz typ efektów ubocznych musi być „przynajmniej” Monadi okazuje się, Monadże wystarczy, aby zaimplementować wszystko, czego do tej pory potrzebowaliśmy.

Druga połowa brzmi: jaka jest najbardziej szczegółowa struktura, jaką możemy nadać „możliwym skutkom ubocznym”? Z pewnością możemy myśleć o przestrzeni wszystkich możliwych skutków ubocznych jako o zbiorze (jedyna operacja, która wymaga członkostwa). Możemy połączyć dwa efekty uboczne, wykonując je jeden po drugim, a to spowoduje inny efekt uboczny (lub być może ten sam - jeśli pierwszym było „wyłączenie komputera”, a drugim „zapis pliku”), to wynik komponowania to po prostu „wyłącz komputer”).

Ok, więc co możemy powiedzieć o tej operacji? To skojarzeniowe; to znaczy, jeśli połączymy trzy efekty uboczne, nie ma znaczenia, w jakiej kolejności wykonamy łączenie. Jeśli to zrobimy (zapisujemy plik, a potem odczytujemy gniazdo), a następnie wyłączamy komputer, jest to to samo, co wykonywanie zapisu pliku następnie (odczyt gniazda, a następnie zamknięcie komputer). Ale to nie jest przemienne: („zapisz plik”, a następnie „usuń plik”) jest efektem ubocznym innym niż („usuń plik”, a następnie „zapisz plik”). I mamy tożsamość: specjalny efekt uboczny „brak efektów ubocznych” działa („brak efektów ubocznych”, a następnie „usuń plik” jest tym samym efektem ubocznym, co zwykłe „usuń plik”). W tym momencie każdy matematyk myśli „Grupuj!” Ale grupy mają odwrotności i ogólnie nie ma sposobu na odwrócenie efektu ubocznego; "usunąć plik" jest nieodwracalne. Tak więc struktura, którą zostawiliśmy, jest monoidem, co oznacza, że ​​nasze funkcje powodujące skutki uboczne powinny być monadami.

Czy istnieje bardziej złożona struktura? Pewnie! Moglibyśmy podzielić możliwe efekty uboczne na efekty oparte na systemie plików, efekty sieciowe i inne, a także moglibyśmy wymyślić bardziej rozbudowane reguły kompozycji, które zachowałyby te szczegóły. Ale znowu sprowadza się to do: Monadjest bardzo prosta, a jednocześnie wystarczająco mocna, aby wyrazić większość właściwości, na których nam zależy. (W szczególności asocjatywność i inne aksjomaty pozwalają nam przetestować naszą aplikację na małych fragmentach, mając pewność, że skutki uboczne połączonej aplikacji będą takie same, jak kombinacja skutków ubocznych elementów).

Właściwie to całkiem czysty sposób myślenia o I / O w funkcjonalny sposób.

W większości języków programowania wykonujesz operacje wejścia / wyjścia. W Haskell wyobraź sobie pisanie kodu nie po to, by wykonywać operacje, ale żeby wygenerować listę operacji, które chciałbyś wykonać.

Monady są po prostu ładną składnią dokładnie do tego.

Jeśli chcesz wiedzieć, dlaczego monady w przeciwieństwie do czegoś innego, myślę, że odpowiedzią jest to, że są one najlepszym funkcjonalnym sposobem reprezentowania I / O, o jakim ludzie mogli pomyśleć, kiedy tworzyli Haskell.

AFAIK, powodem jest możliwość włączenia kontroli skutków ubocznych do systemu typów. Jeśli chcesz dowiedzieć się więcej, posłuchaj tych odcinków SE-Radio : Odcinek 108: Simon Peyton Jones on Functional Programming i Haskell Odcinek 72: Erik Meijer on LINQ

Powyżej znajdują się bardzo dobre, szczegółowe odpowiedzi wraz z podstawami teoretycznymi. Ale chcę przedstawić mój pogląd na monadę IO. Nie jestem doświadczonym programistą haskell, więc może jest to dość naiwne lub nawet złe. Ale pomogłem mi w pewnym stopniu poradzić sobie z monadą IO (zauważ, że nie ma to związku z innymi monadami).

Po pierwsze, chcę powiedzieć, że przykład z „prawdziwym światem” nie jest dla mnie zbyt jasny, ponieważ nie możemy uzyskać dostępu do jego (rzeczywistego świata) poprzednich stanów. Być może nie odnosi się to w ogóle do obliczeń monad, ale jest pożądane w sensie przezroczystości referencyjnej, która jest generalnie obecna w kodzie haskella.

Dlatego chcemy, aby nasz język (haskell) był czysty. Ale potrzebujemy operacji wejścia / wyjścia, ponieważ bez nich nasz program nie może być użyteczny. A te operacje nie mogą być czyste z natury. Więc jedynym sposobem, aby sobie z tym poradzić, jest oddzielenie nieczystych operacji od reszty kodu.

Nadchodzi monada. Właściwie nie jestem pewien, czy nie może istnieć inna konstrukcja o podobnych potrzebnych właściwościach, ale chodzi o to, że monada ma te właściwości, więc może być używana (i jest używana z powodzeniem). Główną własnością jest to, że nie możemy od tego uciec. Interfejs monady nie ma operacji, aby pozbyć się monady wokół naszej wartości. Inne monady (nie we / wy) zapewniają takie operacje i pozwalają na dopasowywanie wzorców (np. Może), ale te operacje nie są wykonywane w interfejsie monady. Kolejną wymaganą właściwością jest możliwość łańcuchowego wykonywania operacji.

Jeśli myślimy o tym, czego potrzebujemy w kategoriach systemu typów, dochodzimy do tego, że potrzebujemy typu z konstruktorem, który można owinąć wokół dowolnej doliny. Konstruktor musi być prywatny, ponieważ zabraniamy ucieczki z niego (tj. Dopasowywania wzorców). Ale potrzebujemy funkcji, aby umieścić wartość w tym konstruktorze (tutaj przychodzi na myśl powrót). Potrzebujemy sposobu na łańcuchowe operacje. Jeśli zastanowimy się nad tym przez jakiś czas, dojdziemy do tego, że operacja łańcuchowa musi mieć typ >> = has. Dochodzimy więc do czegoś bardzo podobnego do monady. Myślę, że jeśli teraz przeanalizujemy możliwe sytuacje sprzeczne z tą konstrukcją, dojdziemy do aksjomatów monad.

Zwróć uwagę, że opracowany konstrukt nie ma nic wspólnego z zanieczyszczeniem. Ma tylko właściwości, które chcieliśmy mieć do czynienia z nieczystymi operacjami, a mianowicie brak ucieczki, łańcuch i sposób na dostanie się do środka.

Teraz pewien zestaw nieczystych operacji jest predefiniowany przez język w tej wybranej monadzie IO. Możemy łączyć te operacje, aby tworzyć nowe nieprzejrzyste operacje. Wszystkie te operacje będą musiały mieć IO w swoim typie. Należy jednak zauważyć, że obecność IO w typie jakiejś funkcji nie czyni tej funkcji zanieczyszczoną. Ale jak rozumiem, pisanie czystych funkcji z IO w ich typie jest złym pomysłem, ponieważ początkowo naszym pomysłem było oddzielenie funkcji czystych od nieczystych.

Na koniec chcę powiedzieć, że monada nie zamienia nieczystych operacji w czyste. Pozwala tylko skutecznie je rozdzielić. (Powtarzam, że to tylko moje zrozumienie)