In welchem Sinne ist die IO-Monade rein?

Question

Man hat mir die IO-Monade als eine Zustandsmonade beschrieben, bei der der Zustand "die reale Welt" ist. Die Befürworter dieses Ansatzes für IO argumentieren, dass dies IO-Operationen rein, d. h. referenziell transparent macht. Warum ist das so? Aus meiner Sicht scheint es, dass Code innerhalb der IO-Monade viele beobachtbare Seiteneffekte hat. Ist es nicht auch möglich, so ziemlich jede nicht-reine Funktion wie eine Funktion der realen Welt zu beschreiben? Können wir uns zum Beispiel malloc in C als eine Funktion vorstellen, die eine RealWorld und einem Int und gibt einen Zeiger und einen RealWorld , nur dass genau wie in der IO-Monade die RealWorld implizit ist?

Hinweis: Ich weiß, was eine Monade ist und wie sie verwendet wird. Bitte antworten Sie nicht mit einem Link zu einem beliebigen Monad-Tutorial, es sei denn, es geht speziell auf meine Frage ein.

Answer 1

Auch wenn der Titel etwas seltsam ist (da er nicht genau zum Inhalt passt), enthält der folgende haskell-cafe Thread eine nette Diskussion über verschiedene IO-Modelle für Haskell.

http://www.mail-archive.com/haskell-cafe@haskell.org/msg79613.html

Answer 2

Nun, das ist es, was man uns an der Universität beigebracht hat.

Eine Funktion ist referenziell transparent, wenn sie für eine bestimmte Eingabe immer denselben Wert zurückgibt (oder derselbe Ausdruck im selben Kontext immer zum selben Wert führt). Daher kann zum Beispiel getChar wäre nicht referenziell transparent, wenn es nur eine Typsignatur hätte () -> Char o Char da Sie unterschiedliche Ergebnisse erhalten können, wenn Sie diese Funktion mehrmals mit demselben Argument aufrufen.

Wenn Sie aber IO monad einführen, dann getChar kann den Typ IO Char und dieser Typ hat nur einen einzigen Wert - IO Char . Also getChar immer denselben Wert, unabhängig davon, welche Taste der Benutzer tatsächlich gedrückt hat.

Aber Sie können immer noch den zugrunde liegenden Wert aus diesem Wert "herausholen". IO Char Sache. Nun, nicht wirklich bekommen, sondern mit dem Bindungsoperator an eine andere Funktion übergeben ( >>= ), so dass Sie mit dem vom Benutzer eingegebenen Zeichen in Ihrem Programm weiterarbeiten können.

Answer 3

Philip Wadler schreibt:

In einer unreinen Sprache kann eine Operation wie tick würde durch eine Funktion des Typs
() -> () . Das fadenscheinige Argument () ist erforderlich, um die Wirkung zu verzögern, bis die Funktion angewendet wird, und da der Ausgabetyp () kann man vermuten, dass der Zweck der Funktion in einem Nebeneffekt liegt. Im Gegensatz dazu ist hier tick hat Typ M () : Es ist kein Scheinargument erforderlich, und das Aussehen von M ausdrücklich darauf hinweist, welche Art von Wirkung auftreten kann .

Ich kann nicht verstehen, wie M () macht die leere Argumentliste () weniger fadenscheinig, aber Wadler ist ziemlich klar, dass Monaden weisen nur auf eine Art von Nebeneffekt hin, sie beseitigen ihn nicht .

Answer 4

In welchem Sinne ist die monadische IO reinem Typ?

In dem Sinne, dass die Werte der IO Typs sind Teile von Standard ML abstrakter imperativer Code die im Idealfall nur vom RTS einer Haskell-Implementierung verarbeitet werden können - in Wie man einen Imperativ deklariert gibt Philip Wadler einen Hinweis darauf, wie dies möglich ist:

(* page 26 *)
type 'a io   = unit -> 'a

infix >>=
val >>=      : 'a io * ('a -> 'b io) -> 'b io
fun m >>= k  = fn () => let
                          val x = m ()
                          val y = k x ()
                        in
                          y
                        end

val return   : 'a -> 'a io
fun return x = fn () => x

(* page 27 *)
val execute : unit io -> unit
fun execute m = m ()

Allerdings, nicht jeder findet diese Situation akzeptabel:

[...] ein zustandsloses Berechnungsmodell auf der Grundlage einer Maschine, deren wichtigste bedeutet], dass die Kluft zwischen Modell und Maschine groß und daher kostspielig zu überbrücken ist. [...]
Dies wurde rechtzeitig auch von den Protagonisten der funktionalen Sprachen erkannt. Sie haben auf verschiedene trickreiche Arten Zustände (und Variablen) eingeführt. Der rein funktionale Charakter wurde dabei kompromittiert und geopfert. [...]

Niklaus Wirth.

...jeder für Miranda (R)?

---

Mir wurde die IO-Monade als eine Zustandsmonade beschrieben, bei der der Zustand "die reale Welt" ist.

Das wäre der Klassiker Pass-the-Planet Modell der E/A, das Sauber direkt verwendet:

import StdFile
import StdMisc
import StdString

Start :: *World -> *World
Start w = putString "Hello, world!\n" w

putString :: String *World -> *World
putString str world
    # (out, world1) = stdio world
    # out1          = fwrites str out
    # (_, world2)   = fclose out1 world1
    = world2

putChar :: Char *World -> *World
putChar c w = putString {c} w

Die Befürworter dieses Ansatzes für E/A argumentieren, dass dies E/A-Operationen rein, d. h. referenziell transparent macht. Warum ist das so?

Denn es ist in der Regel richtig.

Aus dem Standardmodul der Haskell 2010 Bibliothek Daten.Liste :

mapAccumL _ s []        =  (s, [])
mapAccumL f s (x:xs)    =  (s'',y:ys)
                           where (s', y ) = f s x
                                 (s'',ys) = mapAccumL f s' xs

Wenn dieses Idiom so weit verbreitet ist, dass es spezifische Definitionen gibt, die es unterstützen, dann ist seine Verwendung als Modell für E/A (mit einem geeigneten Zustandstyp) wirklich keine große Überraschung - auf den Seiten 14-15 von Zustand in Haskell von John Launchbury und Simon Peyton Jones:

Wie werden dann die E/A-Operationen überhaupt ausgeführt? Die Bedeutung des gesamten Programms wird durch den Wert des Top-Level-Bezeichners mainIO :

mainIO :: IO ()

mainIO ist ein E/A-Zustandstransformator, der vom Betriebssystem auf den Zustand der externen Welt angewendet wird. das Betriebssystem. Semantisch ausgedrückt, gibt er einen neuen Weltzustand zurück, und die Die darin enthaltenen Änderungen werden auf die reale Welt angewandt.

(...damals, als main wurde genannt mainIO .)

Die jüngste Bericht über saubere Sprache ( E/A in der Welt der Einzigartigkeit auf Seite 24 von 148) geht näher darauf ein:

Die Welt, die dem ursprünglichen Ausdruck gegeben wird, ist eine abstrakte Datenstruktur an abstrakte Welt vom Typ *World die Modelle die konkrete physische Welt aus der Sicht des Programms. Die abstrakte Welt kann im Prinzip enthalten alles was ein funktionales Programm benötigt, um während der Ausführung mit der konkreten Welt zu interagieren. Die Welt kann gesehen werden als ein Staat und Veränderungen in der Welt können durch Zustandsübergangsfunktionen auf der Welt oder einem Teil der Welt definiert. Durch dass diese Zustandsübergangsfunktionen auf einer einzigartig Welt können die Veränderungen in der abstrakten Welt direkt in der realen physischen Welt ohne Effizienzverlust und ohne Verlust an referenzieller Transparenz umgesetzt werden.

In Bezug auf die Semantik ist der entscheidende Punkt folgender: Damit die Änderungen eines E/A-zentrierten Programms wirksam werden, muss es sich um ein Programm handeln, das Programm muss den endgültigen Wert des Weltzustands zurückgeben .

Betrachten Sie nun dieses kleine Clean-Programm:

Start :: *World -> *World
Start w = loopX w

loopX :: *World -> *World
loopX w
    # w1 = putChar 'x' w
    = loopX w1

Offensichtlich das Finale World Wert wird nie zurückgegeben, so dass 'x' sollte überhaupt nicht gesehen werden...

Ist es nicht auch möglich, so ziemlich jede nicht reine Funktion wie eine Funktion der realen Welt zu beschreiben?

Ja, so funktioniert das FFI in Haskell 2010 mehr oder weniger.

---

Aus meiner Sicht scheint es, dass Code innerhalb der monadischen IO Typ haben viele beobachtbare Nebenwirkungen.

Wenn Sie GHC verwenden, ist es keine Erscheinung - von Eine Geschichte von Haskell (Seite 26 von 55) von Paul Hudak, John Hughes, Simon Peyton Jones und Philip Wadler:

Natürlich gibt GHC die Welt nicht wirklich weiter; stattdessen wird ein Dummy-"Token" übergeben, um eine korrekte Reihenfolge der Aktionen in Anwesenheit von fauler Auswertung zu gewährleisten, und führt Input und Output als tatsächliche Nebeneffekte aus!

Aber das ist nur ein Detail bei der Umsetzung:

Eine IO Berechnung ist eine Funktion, die (logischerweise) den Zustand der Welt annimmt und eine veränderte Welt sowie den Rückgabewert zurückgibt.

Die Logik gilt nicht für die reale Welt.

Marvin Lee Minsky.