Il mplus deve sempre essere associativo? Haskell wiki vs Oleg Kiselyov

Question

Il Haskell wikibook afferma che

istanze di MonadPlus sono tenuti a soddisfare diverse regole, proprio come le istanze di Monade sono tenuti a soddisfare le tre leggi monade. ... Il più essenziale è che mzero e mplus formano un monoide.

Una conseguenza di questo è che mplus deve essere associativo. Il Haskell wiki è d'accordo.

Tuttavia, Oleg, in one of his many backtracking search implementations, scrive che

-- Generally speaking, mplus is not associative. It better not be, 
-- since associative and non-commutative mplus makes the search 
-- strategy incomplete. 

E 'kosher per definire un non-associativa mplus? I primi due link suggeriscono chiaramente di non avere una vera istanza MonadPlus se mplus non è associativo. Ma se Oleg lo fa ... (D'altra parte, in quel file ha appena la definizione di una funzione chiamata mplus, e non pretendere che chemplus è la mplus di MonadPlus. Ha scelto un nome piuttosto confusa, se questa è la giusta interpretazione.)

Answer 1

Le due leggi che tutti sono d'accordo che MonadPlus devono ubbidire sono le leggi di identità e l'associatività (aka le leggi monoide):

mplus mempty a = a 

mplus a mempty = a 

mplus (mplus a b) c = mplus a (mplus b c) 

ho sempre presumo che hanno in tutti i MonadPlus istanze che io uso e considero istanze che violare tali leggi per essere "infrante", indipendentemente dal fatto che siano state scritte da Oleg.

Oleg ha ragione che l'associatività non funziona bene con la ricerca in ampiezza, ma ciò significa semplicemente che MonadPlus non è l'astrazione che sta cercando.

Per rispondere al punto che hai inserito in un commento, considererei sempre la regola di riscrittura del tuo suono.

Answer 2

È raro che le istanze di MonadPlus violino l'associatività, ma chiaramente non impossibile. I Typeclasses possono essere contati solo per soddisfare le leggi "ovvie" fino a una certa quantità. Ad esempio, quattro ulteriori serie di possibili leggi per MonadPlusare discussed here senza alcuna conclusione e con le librerie che seguono varie convenzioni senza specificare quale.

Chiaramente, Oleg ha un motivo per respingere l'associatività. È "veramente un'istanza MonadPlus"? Chissà, non è definito abbastanza bene da dire.

Answer 3

Di seguito è l'opinione di Oleg stesso, con il mio commento e il suo chiarimento.

O.K. Per prima cosa vorrei registrare il mio disaccordo con Gabriel Gonzalez. Non tutti sono d'accordo sul fatto che MonadPlus deve essere monoid con rispetto a mplus e mzero. Il rapporto non dice nulla al riguardo. Lì sono molti casi convincenti quando questo non è così (vedi sotto). Generalmente, la struttura algebrica dovrebbe adattarsi all'attività. Ecco perché abbiamo gruppi e anche semi-gruppi o groupoids più deboli (magmi).Sembra che MonadPlus sia spesso considerato come una monade di ricerca/non-determinismo. In tal caso, le proprietà di MonadPlus devono essere quelle che facilitano la ricerca e il ragionamento di sulla ricerca, piuttosto che alcune proprietà ideali ad hoc a cui piace qualcuno per qualsiasi motivo. Vi faccio un esempio: si è tentati di porre la legge

m >> mzero === mzero 

Tuttavia, monadi che supportano la ricerca e in grado di fare altri effetti (si pensi NonDeT m) non può soddisfare tale legge. Ad esempio,

print "OK" >> mzero =/== mzero 

perché la stampa lato sinistro qualcosa, ma il destro non lo fa. Allo stesso modo, mplus non può essere simmetrico: mplus m1 m2 generalmente diverso da mplus m2 m1, nello stesso modello.

Veniamo a mplus. Ci sono due ragioni principali per NON richiedere mplus essere associativi. La prima è la completezza della ricerca. Considera

ones = return 1 `mplus` ones 

foo = ones `mplus` return 2 
    === {- inlining ones -} 
    (return 1 `mplus` ones) `mplus` return 2 
    === {- associativity -} 
    return 1 `mplus` (ones `mplus` return 2) 
    === 
    return 1 `mplus` foo 

Sembrerebbe quindi, coincivamente e foo sono gli stessi. Che significhi, non otterremo mai la risposta 2 da pippo.

Questi risultati sono validi per TUTTA la ricerca che può essere rappresentata da MonadPlus, quindi lungo come mplus è associativo e non commutativo. Pertanto, se MonadPlus è una monade per la ricerca, l'associatività di mplus è un requisito irragionevole.

Ecco la seconda ragione: a volte desideriamo una ricerca probabilistica - o, in generale, ricerca ponderata, quando alcune alternative sono ponderate . È ovvio che l'operatore di scelta probabilistica non è associativo. Per questo motivo, il nostro documento JFP evita in particolare la struttura di imponente monoid (mplus, mzero) su MonadPlus.

http://okmij.org/ftp/Computation/monads.html#lazy-sharing-nondet (vedere la discussione sulla figura 1 del documento).

R.C. Penso che Gabriel e tu sia d'accordo sul fatto che le monadi di ricerca non mostrano la struttura monoidale . L'argomento si riduce a se MonadPlus deve essere utilizzato per le ricerche monad o dovrebbe esserci un'altra classe , chiamiamola MonadPlus', che è proprio come MonadPlus ma con leggi più lassiste. Come dici tu, il rapporto non dice nulla su questo argomento e non c'è alcuna autorità da decidere.

Ai fini del ragionamento, non vedo alcun problema con questo - uno deve semplicemente indicare chiaramente le sue ipotesi sulle istanze MonadPlus.

Per quanto riguarda la regola di riscrittura che ri-soci mplus 'Es, la mera esistenza e l'uso diffuso di MonadPlus istanze che non sono associative, indipendentemente dal fatto che siano 'spezzato', significa che si dovrebbe probabilmente astenersi dal definendolo.

O.K. immagino non sono d'accordo con la dichiarazione di Gabriel

Le leggi monoid sono il requisito minimo perché senza di loro le altre leggi sono prive di significato. Ad esempio, quando dici mzero >>= f = mzero, per prima cosa hai bisogno di una definizione ragionevole di mzero, ma senza le leggi sull'identità non hai questo. Le leggi monoidi sono ciò che mantiene "oneste" le altre leggi proposte. Se non hai leggi monoide allora non hai leggi sensate e qual è il punto di una classe di tipo teorico che non ha leggi?

Ad esempio, carta LogicT e soprattutto la carta JFP ha molti esempi di ragionamento equazionale su non-determinismo senza associatività di mplus. Il documento JFP omette tutte le leggi monoid per mplus e mzero (ma utilizza mzero >>= f === mzero). Sembra che uno possa avere "onesto" e "leggi sensibili" per non determinismo e ricerca senza le leggi monoidi per mplus e mzero.

Sono anche sicuro che non sono d'accordo con l'affermazione

Le due leggi che tutti sono d'accordo che MonadPlus dovrebbe obbedire sono alle leggi di identità e l'associatività (aka le leggi monoide):

Non sono sicuro che sia stato effettuato un sondaggio su questo. Il rapporto non afferma leggi per mplus (forse gli autori stavano ancora discutendo di loro). Quindi, io direi che il problema è aperto - e questo è il messaggio principale per ottenere attraverso.