haskell - learn - monad example

¿Debe mplus siempre ser asociativo? Haskell wiki contra Oleg Kiselyov

Question

El wikibook de Haskell afirma que

Las instancias de MonadPlus deben cumplir varias reglas, al igual que las instancias de Monad deben cumplir las tres leyes de la mónada ... Lo más esencial es que mzero y mplus forman un monoide.

Una consecuencia de esto es que mplus debe ser asociativo. La wiki de Haskell está de acuerdo.

Sin embargo, Oleg, en una de sus muchas implementaciones de búsqueda de seguimiento , escribe que

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

¿Es kosher definir un mplus no asociativo? Los dos primeros enlaces sugieren claramente que no tiene una instancia real de MonadPlus si mplus no es asociativo. Pero si Oleg lo hace ... (Por otro lado, en ese archivo solo está definiendo una función llamada mplus , y no afirma que ese mplus sea ​​el mplus de MonadPlus . Él eligió un nombre bastante confuso, si es el correcto interpretación.)

Answer 1

A continuación se muestra la opinión del propio Oleg, con mi comentario y su aclaración.

Bueno, primero me gustaría registrar mi desacuerdo con Gabriel González. No todos están de acuerdo en que MonadPlus debe ser monoide con respecto a mplus y mzero . El informe no dice nada al respecto. Hay muchos casos convincentes cuando esto no es así (ver más abajo). Generalmente, la estructura algebraica debe encajar en la tarea. Es por eso que tenemos grupos, y también semi-grupos más débiles o groupoids (magmas). Parece que MonadPlus es a menudo considerado como una mónada de búsqueda / no determinismo. Si es así, entonces las propiedades de MonadPlus deben ser aquellas que faciliten la búsqueda y el razonamiento sobre la búsqueda, en lugar de algunas propiedades ad hoc ideales que a alguien le gustan por cualquier motivo. Déjame dar un ejemplo: es tentador postular la ley.

m >> mzero === mzero

Sin embargo, las mónadas que admiten la búsqueda y pueden hacer otros efectos (piense en NonDeT m ) no pueden satisfacer esa ley. Por ejemplo,

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

porque el lado izquierdo imprime algo, pero el lado derecho no lo hace. De la misma manera, mplus no puede ser simétrico: mplus m1 m2 generalmente difiere de mplus m2 m1 , en el mismo modelo.

Vengamos a mplus . Hay dos razones principales para NO requerir que mplus sea ​​asociativo. Primero está la integridad de la búsqueda. Considerar

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

Parecería por lo tanto, coinductivamente unos y otros son lo mismo. Eso significa que nunca obtendremos la respuesta 2 de foo.

Los resultados se mantienen para CUALQUIER búsqueda que pueda ser representada por MonadPlus , siempre que mplus sea ​​asociativa y no conmutativa. Por lo tanto, si MonadPlus es una mónada para búsqueda, entonces la asociatividad de mplus es un requisito irrazonable.

Esta es la segunda razón: a veces deseamos una búsqueda probabilística o, en general, una búsqueda ponderada, cuando se ponderan algunas alternativas. Es obvio que el operador de elección probabilística no es asociativo. Por esa razón, nuestro documento de JFP específicamente evita la imposición de la estructura de MonadPlus ( mplus , mzero ) en MonadPlus .

http://okmij.org/ftp/Computation/monads.html#lazy-sharing-nondet (consulte la discusión en la Figura 1 del documento).

RC : Creo que Gabriel y usted están de acuerdo en el hecho de que las mónadas de búsqueda no exhiben la estructura monoide. El argumento se reduce a si MonadPlus debe usarse para buscar mónadas o si debería haber otra clase, llamémosla MonadPlus'' , que es igual que MonadPlus pero con leyes más laxas. Como usted dice, el informe no dice nada sobre este tema, y ​​no hay autoridad para decidir.

Con el propósito de razonar, no veo ningún problema con eso, solo hay que indicar claramente sus suposiciones sobre las instancias de MonadPlus .

En cuanto a la regla de reescritura que vuelve a asociar a mplus , la mera existencia y el uso generalizado de MonadPlus instancias de MonadPlus que no son asociativas, independientemente de si están "rotas", significa que uno debe abstenerse de definirlas.

OK , supongo que no estoy de acuerdo con la declaración de Gabriel

Las leyes monoides son el requisito mínimo porque sin ellas las otras leyes carecen de significado. Por ejemplo, cuando dices mzero >>= f = mzero , primero necesitas una definición sensata de mzero , pero sin las leyes de identidad no tienes eso. Las leyes monoides son las que mantienen a las demás leyes propuestas "honestas". Si no tiene las leyes monoides, entonces no tiene leyes sensibles y ¿qué sentido tiene una clase de tipo teórico que no tiene leyes?

Por ejemplo, el papel de LogicT y especialmente el de JFP tiene muchos ejemplos de razonamiento ecuacional sobre el no determinismo, sin asociatividad de mplus . El documento de JFP omite todas las leyes de mplus para mplus y mzero (pero usa mzero >>= f === mzero ). Parece que uno puede tener "leyes honestas" y "honestas" para el no determinismo y buscar sin las leyes mplus para mplus y mzero .

Tampoco estoy seguro de estar de acuerdo con el reclamo

Las dos leyes que todos están de acuerdo en que MonadPlus debe obedecer son las leyes de identidad y asociatividad (también conocidas como leyes monoides):

No estoy seguro de que se haya hecho una encuesta sobre esto. El Informe no establece leyes para mplus (quizás los autores todavía los estaban debatiendo). Por lo tanto, diría que el problema está abierto, y este es el mensaje principal que se debe transmitir.

Answer 2

Es raro que MonadPlus instancias de MonadPlus violen la asociatividad, pero claramente no es imposible. Las clases de tipos solo se pueden contar para cumplir con las leyes "obvias" hasta una cierta cantidad. Por ejemplo, cuatro conjuntos adicionales de leyes posibles para MonadPlus se discuten aquí sin ninguna conclusión y con las bibliotecas siguiendo varias convenciones sin especificar cuál.

Claramente, Oleg tiene una razón para rechazar la asociatividad. ¿Es "realmente una instancia de MonadPlus "? Quién sabe, no está lo suficientemente definido como para decirlo.

Answer 3

Las dos leyes que todos están de acuerdo en que MonadPlus debe obedecer son las leyes de identidad y asociatividad (también conocidas como leyes monoides):

mplus mempty a = a

mplus a mempty = a

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

Siempre asumo que tienen en todas MonadPlus instancias de MonadPlus que utilizo y considero que las instancias que violan esas leyes están "violadas", hayan sido o no escritas por Oleg.

Oleg tiene razón al MonadPlus que la asociatividad no juega bien con la primera búsqueda de amplitud, pero eso solo significa que MonadPlus no es la abstracción que está buscando.

Para responder al punto que hizo en un comentario, siempre consideraría que su regla de reescritura es suya.