Czy monada IO jest technicznie niepoprawna?

12

Na wiki haskell znajduje się następujący przykład warunkowego użycia monady IO (patrz tutaj) .

when :: Bool -> IO () -> IO ()
when condition action world =
    if condition
      then action world
      else ((), world)

Zauważ, że w tym przykładzie IO aprzyjęto definicję, RealWorld -> (a, RealWorld)aby wszystko było bardziej zrozumiałe.

Ten fragment kodu warunkowo wykonuje akcję w monadzie we / wy. Zakładając, że tak conditionjest False, akcja actionnigdy nie powinna zostać wykonana. Przy użyciu leniwej semantyki tak właśnie byłoby. Należy jednak zauważyć , że Haskell z technicznego punktu widzenia nie jest ścisły. Oznacza to, że kompilator może na przykład zapobiegawczo uruchamiać action worldsię w innym wątku, a później wyrzucić to obliczenie, gdy odkryje, że go nie potrzebuje. Jednak do tego momentu działania niepożądane już się wydarzyły.

Teraz można zaimplementować monadę we / wy w taki sposób, że skutki uboczne są propagowane dopiero po zakończeniu całego programu i wiemy dokładnie, jakie skutki uboczne należy wykonać. Nie dzieje się tak jednak, ponieważ w Haskell można pisać nieskończone programy, które wyraźnie mają pośrednie skutki uboczne.

Czy to oznacza, że ​​monada IO jest technicznie niepoprawna, czy może jest coś innego, co mogłoby temu zapobiec?

Lasse
źródło
Witamy w informatyce ! Twoje pytanie jest tutaj nie na temat: mamy do czynienia z komputerem naukowych pytań, a nie programowania pytania (patrz nasz FAQ ). Twoje pytanie może dotyczyć przepełnienia stosu .
dkaeae
2
Moim zdaniem jest to pytanie informatyczne, ponieważ dotyczy teoretycznej semantyki Haskella, a nie praktycznego pytania programistycznego.
Lasse
4
Nie jestem zbyt zaznajomiony z teorią języka programowania, ale myślę, że to pytanie jest tutaj na temat. Pomocne może być wyjaśnienie, co tutaj oznacza „zło”. Jak myślisz, jaką właściwość ma monada IO, której nie powinna mieć?
Dyskretna jaszczurka
1
Ten program nie jest dobrze napisany. Nie jestem pewien, co tak naprawdę chciałeś napisać. Definicja whenjest typowalna, ale nie ma deklarowanego typu i nie wiem, co czyni ten kod interesującym.
Gilles „SO - przestań być zły”
2
Ten program jest pobierany dosłownie ze strony Haskell-wiki, do której link znajduje się bezpośrednio powyżej. Rzeczywiście nie pisze. Wynika to z tego, że jest napisane przy założeniu, że IO ajest zdefiniowane jako RealWorld -> (a, RealWorld), aby uczynić elementy wewnętrzne IO bardziej czytelnymi.
Lasse

Odpowiedzi:

12

Jest to sugerowana „interpretacja” IOmonady. Jeśli chcesz poważnie potraktować tę „interpretację”, musisz poważnie potraktować „RealWorld”. Nie ma znaczenia, czy action worldzostanie spekulacyjnie oceniony, czy nie, actionnie ma żadnych skutków ubocznych, jego ewentualne skutki są obsługiwane przez zwrócenie nowego stanu wszechświata, w którym wystąpiły te efekty, np. Wysłano pakiet sieciowy. Jednak wynikiem tej funkcji jest ((),world)nowy stan wszechświata world. Nie używamy nowego wszechświata, który mogliśmy spekulować na boku. Stan wszechświata jest world.

Prawdopodobnie trudno ci brać to na poważnie. Jest na wiele sposobów, w najlepszym wypadku, powierzchownie paradoksalny i bezsensowny. Z tej perspektywy współbieżność jest albo nieoczywista, albo szalona.

„Czekaj, czekaj” - mówisz. „ RealWorldto tylko„ token ”. To nie jest stan całego wszechświata.” Okej, to ta „interpretacja” nic nie wyjaśnia. Niemniej jednak, jako szczegół implementacji , tak właśnie modele GHC IO. 1 Oznacza to jednak, że mamy magiczne „funkcje”, które faktycznie wywołują skutki uboczne i ten model nie zawiera wskazówek co do ich znaczenia. A ponieważ te funkcje faktycznie wywołują skutki uboczne, twoja obawa jest całkowicie na miejscu. GHC nie trzeba wychodzić z jego sposób, aby upewnić się RealWorld, a te specjalne funkcje nie są zoptymalizowane w taki sposób, że zmiany zamierzonego zachowania programu.

Osobiście (jak to zapewne jest obecnie widoczne), uważam, że ten „przemijający świat” model IOjest po prostu bezużyteczny i mylący jako narzędzie pedagogiczne. (Nie wiem, czy jest to przydatne do implementacji. W przypadku GHC uważam, że jest to raczej historyczny artefakt).

Jednym z alternatywnych podejść jest wyświetlanie IOżądań opisujących za pomocą procedur obsługi odpowiedzi. Można to zrobić na kilka sposobów. Prawdopodobnie najbardziej dostępna jest darmowa konstrukcja monady, w szczególności możemy użyć:

data IO a = Return a | Request OSRequest (OSResponse -> IO a)

Istnieje wiele sposobów, aby uczynić to bardziej wyrafinowanym i mieć nieco lepsze właściwości, ale jest to już poprawa. Nie wymaga głębokich filozoficznych założeń dotyczących natury rzeczywistości. Stwierdza tylko, że IOjest to albo trywialny program Return, który nic nie robi, ale zwraca wartość, albo jest to żądanie do systemu operacyjnego z funkcją obsługi odpowiedzi. OSRequestmoże być coś takiego:

data OSRequest = OpenFile FilePath | PutStr String | ...

Podobnie OSResponsemoże być coś takiego:

data OSResponse = Errno Int | OpenSucceeded Handle | ...

(Jednym z ulepszeń, które mogą być wykonane jest, aby rzeczy bardziej wpisz bezpieczny tak, że wiesz, że nie będzie się OpenSucceededz PutStrwniosku). To modele IOjak opisujący wnioski, które uzyskać interpretowane przez jakiegoś układu (za „prawdziwe” IOmonada jest sam środowisko uruchomieniowe Haskell), a następnie być może ten system wywoła moduł obsługi, którego udzieliliśmy odpowiedzi. To oczywiście nie daje żadnych wskazówek na temat tego, jak PutStr "hello world"należy obsługiwać takie żądanie , ale też nie udaje. Wyjaśnia, że ​​jest to delegowane do innego systemu. Ten model jest również dość dokładny. Wszystkie programy użytkownika we współczesnych systemach operacyjnych muszą wysyłać żądania do systemu operacyjnego, aby cokolwiek zrobić.

Ten model zapewnia właściwe intuicje. Na przykład wielu początkujących uważa rzeczy takie jak <-operator za „rozpakowywanie” IOlub mają (niestety wzmocnione) widoki, które IO String, powiedzmy, są „pojemnikami”, które „zawierają” String(a następnie <-wyciągają je). Ten widok żądanie-odpowiedź sprawia, że ​​ta perspektywa jest wyraźnie błędna. Wewnątrz nie ma uchwytu pliku OpenFile "foo" (\r -> ...). Popularną analogią do podkreślenia tego jest to, że w przepisie na ciasto nie ma ciasta (a może w tym przypadku lepiej byłoby „wystawić fakturę”).

Ten model działa również z współbieżnością. Możemy łatwo mieć konstruktor dla OSRequestlike, Fork :: (OSResponse -> IO ()) -> OSRequesta następnie środowisko wykonawcze może przeplatać żądania wygenerowane przez ten dodatkowy moduł obsługi z normalnym modułem obsługi, jak mu się podoba. Przy odrobinie sprytu możesz użyć tej (lub pokrewnych technik) do modelowania rzeczy takich jak współbieżność bardziej bezpośrednio, niż po prostu mówiąc „wysyłamy zapytanie do systemu operacyjnego i rzeczy się dzieją”. Tak działa IOSpecbiblioteka .

1 Uściski zastosowały kontynuację, IOktóra jest mniej więcej podobna do tego, co opisuję, aczkolwiek z nieprzezroczystymi funkcjami zamiast jawnego typu danych. HBC wykorzystał również implementację opartą na kontynuacji warstwową na starym IO opartym na strumieniu żądanie-odpowiedź. NHC (a tym samym YHC) użył thunksów, tzn. Z grubsza, IO a = () -> ajak ()to się nazywało World, ale nie robi stanu. JHC i UHC zastosowały w zasadzie to samo podejście co GHC.

Derek Elkins opuścił SE
źródło
Dzięki za twoją oświecającą odpowiedź, to naprawdę pomogło. Wdrożenie IO zajęło mi trochę czasu, ale zgadzam się, że jest to bardziej intuicyjne. Czy twierdzisz, że ta implementacja nie cierpi z powodu potencjalnych problemów z porządkowaniem efektów ubocznych, podobnie jak implementacja RealWorld? Nie widzę od razu żadnych problemów, ale nie jest dla mnie jasne, że nie istnieją.
Lasse
Jeden komentarz: wydaje się, że OpenFile "foo" (\r -> ...)tak powinno być Request (OpenFile "foo") (\r -> ...)?
Lasse
@Lasse Tak, powinno być Request. Aby odpowiedzieć na pierwsze pytanie, IOjest to wyraźnie niewrażliwe na kolejność oceny (dna modulo), ponieważ jest to wartość obojętna. Wszystkie skutki uboczne (jeśli występują) byłyby spowodowane przez rzecz, która interpretuje tę wartość. W tym whenprzykładzie nie miałoby znaczenia, gdyby actionzostało ocenione, ponieważ byłaby to po prostu wartość, Request (PutStr "foo") (...)której i tak nie damy rzeczowi interpretującemu te żądania. To jest jak kod źródłowy; nie ma znaczenia, czy zmniejszysz go chętnie czy leniwie, nic się nie dzieje, dopóki nie zostanie przekazane tłumaczowi.
Derek Elkins opuścił SE
Ach tak, widzę to. To naprawdę sprytna definicja. Na początku myślałem, że wszystkie skutki uboczne musiałyby koniecznie wystąpić po zakończeniu działania całego programu, ponieważ musisz zbudować strukturę danych, zanim będziesz mógł ją zinterpretować. Ale ponieważ żądanie zawiera kontynuację, musisz tylko zbudować dane z pierwszego Request, aby zacząć widzieć efekty uboczne. Oceniając kontynuację, można utworzyć kolejne skutki uboczne. Sprytny!
Lasse