Perché gli effetti collaterali sono modellati come monadi in Haskell?

Qualcuno potrebbe dare alcuni suggerimenti sul perché i calcoli impuri in Haskell sono modellati come monadi?

Voglio dire Monad è solo un’interfaccia con 4 operazioni, quindi qual è stato il ragionamento per la modellazione di effetti collaterali in esso?

Supponiamo che una funzione abbia effetti collaterali. Se prendiamo tutti gli effetti che produce come parametri di input e output, allora la funzione è pura per il mondo esterno.

Quindi per una funzione impura

 f' :: Int -> Int 

aggiungiamo il RealWorld alla considerazione

 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. 

allora f è di nuovo puro. Definiamo un tipo di dati parametrizzati IO a = RealWorld -> (a, RealWorld) , quindi non è necessario digitare RealWorld così tante volte

 f :: Int -> IO Int 

Per il programmatore, gestire direttamente un RealWorld è troppo pericoloso, in particolare, se un programmatore mette le mani su un valore di tipo RealWorld, potrebbe provare a copiarlo , il che è praticamente imansible. (Pensa di provare a copiare l’intero filesystem, ad esempio dove lo inseriresti?) Pertanto, la nostra definizione di IO incapsula anche gli stati di tutto il mondo.

Queste funzioni impure sono inutili se non possiamo incatenarle insieme. Prendere in considerazione

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

Vogliamo ottenere un nome file dalla console, leggere quel file, quindi stampare il contenuto. Come lo faremmo se potessimo accedere agli stati del mondo reale?

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

Vediamo un modello qui: le funzioni sono chiamate così:

 ... (, worldY) = f worldX (, worldZ) = g  worldY ... 

Quindi potremmo definire un operatore ~~~ per vincolarli:

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

allora potremmo semplicemente scrivere

 printFile = getLine ~~~ getContents ~~~ putStrLn 

senza toccare il mondo reale.


Ora supponiamo di voler rendere anche il testo del file in maiuscolo. Il sovrascrittura è una funzione pura

 upperCase :: String -> String 

Ma per trasformarlo nel mondo reale, deve restituire una IO String . È facile sollevare una funzione del genere:

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

questo può essere generalizzato:

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

in modo che impureUpperCase = impurify . upperCase impureUpperCase = impurify . upperCase , e possiamo scrivere

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

(Nota: normalmente scriviamo getLine ~~~ getContents ~~~ (putStrLn . upperCase) )


Ora vediamo cosa abbiamo fatto:

  1. Abbiamo definito un operatore (~~~) :: IO b -> (b -> IO c) -> IO c che raggruppa insieme due funzioni impure
  2. Abbiamo definito una funzione impurify :: a -> IO a che converte un valore puro in impuro.

Ora facciamo l’identificazione (>>=) = (~~~) e return = impurify , e vedi? Abbiamo una monade.


(Per verificare se sia davvero una monade ci sono pochi assiomi che dovrebbero essere soddisfatti:

(1) return a >>= f = fa

  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 = fa 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 = fa worldX 

(3) f >>= (\x -> gx >>= h) = (f >>= g) >>= h

Esercizio.)

Qualcuno potrebbe dare alcuni suggerimenti sul perché i calcoli impuri in Haskell sono modellati come monadi?

Questa domanda contiene un malinteso diffuso. Impurità e Monade sono nozioni indipendenti. L’impurità non è modellata da Monad. Piuttosto, ci sono alcuni tipi di dati, come IO , che rappresentano il calcolo imperativo. E per alcuni di questi tipi, una piccola parte della loro interfaccia corrisponde al modello di interfaccia chiamato “Monad”. Inoltre, non vi è alcuna spiegazione pura / funzionale / denotativa conosciuta di IO (ed è improbabile che lo sia, considerando lo scopo “sin bin” di IO ), sebbene ci sia la storia comunemente raccontata di World -> (a, World) essere il significato di IO a . Quella storia non può descrivere in modo IO , perché IO supporta la concorrenza e il non-determinismo. La storia non funziona nemmeno quando si tratta di calcoli deterministici che consentono l’interazione mid-computation con il mondo.

Per ulteriori spiegazioni, vedere questa risposta .

Modifica : rileggendo la domanda, non penso che la mia risposta sia abbastanza precisa. I modelli di calcolo imperativo spesso si rivelano monadi, proprio come diceva la domanda. Il richiedente potrebbe non dare per scontato che la monade in qualche modo consenta la modellizzazione del calcolo imperativo.

A quanto ho capito, qualcuno che si chiamava Eugenio Moggi notò per la prima volta che un costrutto matematico precedentemente oscuro chiamato “monade” poteva essere usato per modellare gli effetti collaterali nei linguaggi del computer, e quindi specificare la loro semantica usando il calcolo Lambda. Quando Haskell si stava sviluppando c’erano vari modi in cui venivano modellati i calcoli impuri (vedi la carta “camicia per capelli” di Simon Peyton Jones per maggiori dettagli), ma quando Phil Wadler introdusse le monadi divenne subito ovvio che questa era la risposta. E il resto è storia.

Qualcuno potrebbe dare alcuni suggerimenti sul perché i calcoli impuri in Haskell sono modellati come monadi?

Bene, perché Haskell è puro . È necessario un concetto matematico per distinguere tra calcoli non puri e puri a livello di tipo e per modellizzare i flussi di programma in rispettivamente.

Questo significa che dovrai finire con qualche tipo di I / IO a che modella un calcolo non puro. Quindi è necessario conoscere i modi per combinare questi calcoli di cui applicare in sequenza ( >>= ) e sollevare un valore ( return ) sono quelli più evidenti e di base.

Con questi due, hai già definito una monade (senza nemmeno pensarci);)

Inoltre, le monadi forniscono astrazioni molto generiche e potenti , quindi molti tipi di stream di controllo possono essere convenientemente generalizzati in funzioni liftM come la sequence , il liftM o la syntax speciale, rendendo l’unpureness non un caso così speciale.

Vedere le monadi nella programmazione funzionale e nella tipizzazione dell’unicità (l’unica alternativa che conosco) per maggiori informazioni.

Come dici tu, Monad è una struttura molto semplice. Una metà della risposta è: Monad è la struttura più semplice che potremmo eventualmente dare alle funzioni di effetti collaterali ed essere in grado di usarle. Con Monad possiamo fare due cose: possiamo trattare un valore puro come valore di effetto collaterale ( return ), e possiamo applicare una funzione di effetto collaterale ad un valore di effetto collaterale per ottenere un nuovo valore di effetto collaterale ( >>= ). Perdere la capacità di fare una di queste cose sarebbe paralizzante, quindi il nostro tipo a effetto collaterale deve essere “almeno” Monad , e risulta che Monad è abbastanza per implementare tutto ciò di cui abbiamo avuto bisogno fino ad ora.

L’altra metà è: qual è la struttura più dettagliata che potremmo dare ai “possibili effetti collaterali”? Possiamo certamente pensare allo spazio di tutti i possibili effetti collaterali come set (l’unica operazione che richiede è l’appartenenza). Possiamo combinare due effetti collaterali facendoli uno dopo l’altro, e questo darà origine a un effetto collaterale diverso (o forse lo stesso – se il primo era “computer di spegnimento” e il secondo era “scrivi file”, quindi il risultato di comporre questi è solo “computer di spegnimento”).

Ok, allora cosa possiamo dire di questa operazione? È associativo; cioè, se combiniamo tre effetti collaterali, non importa quale sia l’ordine in cui facciamo la combinazione. Se facciamo (scrivi file poi leggi socket) e spegnilo, è come fare il file di scrittura allora (leggi socket e shutdown computer). Ma non è commutativo: (“scrivi file” quindi “cancella file”) è un effetto collaterale diverso da (“cancella file” quindi “scrivi file”). E abbiamo un’id quadro: l’effetto collaterale speciale “nessun effetto collaterale” funziona (“nessun effetto collaterale”, quindi “elimina il file” è lo stesso effetto collaterale del solo “cancella file”). A questo punto ogni matematico pensa “Gruppo!” Ma i gruppi hanno inversioni e non c’è modo di invertire un effetto collaterale in generale; “elimina file” è irreversibile. Quindi la struttura che abbiamo lasciato è quella di un monoide, il che significa che le nostre funzioni di effetti collaterali dovrebbero essere le monadi.

Esiste una struttura più complessa? Sicuro! Potremmo dividere i possibili effetti collaterali in effetti basati su file system, effetti basati sulla rete e altro, e potremmo elaborare regole di composizione più elaborate che preservassero questi dettagli. Ma ancora una volta si tratta di: Monad è molto semplice, eppure abbastanza potente da esprimere la maggior parte delle proprietà che ci interessano. (In particolare, l’associatività e gli altri assiomi ci permettono di testare la nostra applicazione in piccoli pezzi, con la certezza che gli effetti collaterali dell’applicazione combinata saranno gli stessi della combinazione degli effetti collaterali dei pezzi).

In realtà è un modo abbastanza pulito per pensare all’I / O in modo funzionale.

Nella maggior parte dei linguaggi di programmazione, esegui operazioni di input / output. In Haskell, immagina di scrivere il codice per non eseguire le operazioni, ma per generare un elenco delle operazioni che vorresti fare.

Le Monade sono semplicemente syntax per questo.

Se vuoi sapere perché le monadi sono opposte a qualcos’altro, credo che la risposta sia che sono il modo migliore per rappresentare l’I / O a cui la gente potrebbe pensare quando stavano facendo Haskell.

AFAIK, la ragione è quella di essere in grado di includere i controlli degli effetti collaterali nel sistema di tipi. Se vuoi saperne di più, ascolta gli episodi della SE-Radio : Episodio 108: Simon Peyton Jones su Functional Programming e Haskell Episodio 72: Erik Meijer su LINQ

Sopra ci sono ottime risposte dettagliate con background teorico. Ma voglio dare la mia opinione su IO monade. Non sono un esperto programmatore di haskell, quindi potrebbe essere piuttosto ingenuo o addirittura sbagliato. Ma mi ha aiutato ad affrontare in qualche misura la monade dell’IO (nota che non si riferisce ad altre monadi).

Per prima cosa voglio dire, quell’esempio con “mondo reale” non è troppo chiaro per me in quanto non possiamo accedere ai suoi stati precedenti (nel mondo reale). Può essere che non si riferisca a calcoli monografici ma è desiderato nel senso della trasparenza referenziale, che è generalmente presente nel codice haskell.

Quindi vogliamo che il nostro linguaggio (haskell) sia puro. Ma abbiamo bisogno di operazioni di input / output, perché senza di loro il nostro programma non può essere utile. E quelle operazioni non possono essere pure per loro natura. Quindi l’unico modo per affrontarlo è separare le operazioni impure dal resto del codice.

Qui viene la monade. In realtà, non sono sicuro, che non possa esistere altro costrutto con proprietà simili simili, ma il punto è che monad ha queste proprietà, quindi può essere usato (ed è usato con successo). La proprietà principale è che non possiamo sfuggire a questo. L’interfaccia di Monad non ha operazioni per sbarazzarsi della monade attorno al nostro valore. Altre (non IO) monadi forniscono tali operazioni e consentono la corrispondenza del modello (ad esempio, forse), ma tali operazioni non sono nell’interfaccia di monad. Un’altra proprietà richiesta è la capacità di concatenare le operazioni.

Se pensiamo a ciò di cui abbiamo bisogno in termini di sistema di tipi, arriviamo al fatto che abbiamo bisogno di digitare con il costruttore, che può essere avvolto attorno a qualsiasi valore. Il costruttore deve essere privato, poiché ne vietiamo la fuga (ad esempio la corrispondenza del modello). Ma abbiamo bisogno di una funzione per mettere valore in questo costruttore (qui ritorna in mente). E abbiamo bisogno del modo di concatenare le operazioni. Se ci pensiamo per un po ‘, arriveremo al fatto che l’operazione di concatenazione deve avere tipo come >> = ha. Quindi, arriviamo a qualcosa di molto simile alla monade. Penso che, se analizziamo ora possibili situazioni contraddittorie con questo costrutto, arriveremo agli assiomi monad.

Nota che il costrutto sviluppato non ha nulla in comune con l’impurità. Ha solo proprietà, che noi desideriamo essere in grado di gestire operazioni impure, vale a dire senza sfuggire, concatenare e un modo per entrare.

Ora alcune serie di operazioni impure sono predefinite dalla lingua all’interno di questo monade IO selezionato. Possiamo combinare queste operazioni per creare nuove operazioni non pure. E tutte quelle operazioni dovranno avere IO nel loro tipo. Si noti tuttavia che la presenza di IO nel tipo di alcune funzioni non rende impura questa funzione. Ma come ho capito, è una ctriggers idea scrivere funzioni pure con IO nel loro tipo, poiché inizialmente era nostra idea separare le funzioni pure e impure.

Infine, voglio dire, che la monade non trasforma le operazioni impure in puri. Permette solo di separarli in modo efficace. (Ripeto, che è solo la mia comprensione)