Должен ли mplus всегда быть ассоциативным? Haskell wiki - Олег Киселев

Haskell wikibook утверждает, что

Экземпляры MonadPlus должны выполнять несколько правил, так же как экземпляры Монады необходимы для выполнения трех законов монады.... Самое главное, что mzero и mplus образуют моноид.

Следствием этого является то, что mplus должно быть ассоциативным. Haskell wiki соглашается.

Однако Олег, в одной из своих многочисленных поисковых реализаций поиска backback, пишет, что

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

Кошерно ли определить неассоциативный mplus? Первые две ссылки довольно ясно показывают, что у вас нет реального экземпляра MonadPlus, если mplus не является ассоциативным. Но если Олег делает это... (С другой стороны, в этом файле он просто определяет функцию под названием mplus и не утверждает, что mplus является mplus of MonadPlus. Он выбрал довольно запутанное имя, если это правильная интерпретация.)

Ответ 1

Два закона, которые все согласны с тем, что MonadPlus должны подчиняться, - это законы тождества и ассоциативности (a.k.a. моноидные законы):

mplus mempty a = a

mplus a mempty = a

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

Я всегда предполагаю, что они хранятся во всех экземплярах MonadPlus, которые я использую, и рассматриваю случаи, которые нарушают эти законы, "сломаны", независимо от того, написаны они Олегом или нет.

Олег прав, что ассоциативность не играет хорошо с поиском по ширине, но это означает, что MonadPlus не является абстракцией, которую он ищет.

Чтобы ответить на вопрос, который вы сделали в комментарии, я всегда буду считать, что вы переписываете правило своего звука.

Ответ 2

Ниже приводится мнение самого Олега с моим комментарием и его разъяснениями.

O.K. Сначала я хотел бы зарегистрировать свое несогласие с Габриэлем Гонсалес. Не все согласны с тем, что MonadPlus должен быть моноидным с относительно mplus и mzero. В Отчете ничего не говорится. Там есть много убедительных случаев, когда это не так (см. ниже). В общем, алгебраическая структура должна соответствовать задаче. Вот почему мы имеем групп, а также более слабые полугруппы или группоиды (магмы). Кажется MonadPlus часто рассматривается как монада поиска/недетерминизма. Если так, то свойствами MonadPlus должны быть те, которые облегчают поиск и рассуждение о поиске - а не какой-то идеальный ad hoc свойства кого-то любят по любой причине. Позвольте мне привести пример: заманчиво установить закон

m >> mzero === mzero

Однако, монады, которые поддерживают поиск и могут делать другие эффекты (подумайте NonDeT m) не может удовлетворить этот закон. Например,

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

потому что левая сторона печатает что-то, но правую не делает. Точно так же mplus не может быть симметричным: mplus m1 m2 обычно отличается от mplus m2 m1 в той же модели.

Перейдем к mplus. Есть две основные причины: НЕ требовать mplus быть ассоциативным. Во-первых, полнота поиска. Рассмотрим

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

Казалось бы, коиндуктивные единицы и foo одинаковы. Что значит, мы никогда не получим ответ 2 от foo.

Эти результаты сохраняются для ЛЮБОГО поиска, который может быть представлен MonadPlus, поэтому поскольку mplus является ассоциативным и некоммутативным. Поэтому, если MonadPlus является монады для поиска, то ассоциативность mplus является необоснованным требованием.

Вот вторая причина: иногда мы желаем вероятностного поиск - или, в общем, взвешенный поиск, когда некоторые альтернативы взвешенная. Очевидно, что вероятностный оператор выбора не ассоциативно. По этой причине наш JFP-документ специально избегает наложение моноида (mplus, mzero) на MonadPlus.

http://okmij.org/ftp/Computation/monads.html#lazy-sharing-nondet (см. обсуждение на рисунке 1 статьи).

R.C. Я думаю, что Габриэль и вы согласны с тем, что поисковые монады не проявляют моноидную структуру. Аргумент сводится к тому, MonadPlus следует использовать для поисковых монад или если есть другой класс, пусть назовем его MonadPlus', который похож на MonadPlus, но с более слабых законов. Как вы говорите, в отчете ничего не говорится об этом темы, и нет полномочий для принятия решения.

В целях рассуждения я не вижу никаких проблем с этим - один просто должен четко изложить свои предположения о экземплярах MonadPlus.

Что касается правила перезаписи, которое повторно ассоциирует mplus 'es, то простое существование и широкое использование экземпляров MonadPlus, которые не являются ассоциативными, независимо от того, являются ли они "сломанными", означает, что, вероятно, следует воздерживаться от его определения.

O.K. Думаю, я не согласен с утверждением Габриэля

Моноидные законы являются минимальным требованием, поскольку без них другие законы бессмысленны. Например, когда вы говорите mzero >>= f = mzero, вам сначала нужно какое-то разумное определение mzero есть, но без законов идентичности у вас этого нет. моноидные законы - вот что удерживает другие предложенные законы "честными". Если вы не имеют моноидные законы, тогда у вас нет разумных законов и что точка класса теоретического типа, который не имеет законов?

Например, бумага LogicT и особенно бумага JFP содержат много примеры эквационального рассуждения о недетерминизме, без ассоциативность mplus. В документе JFP отсутствуют все моноидные законы для mplus и mzero (но использует mzero >>= f === mzero). Кажется, что можно "честных" и "разумных законов" для детерминизма и поиска без моноидные законы для mplus и mzero.

Я также не уверен, что согласен с выражением

Два закона, которые все согласны с тем, что MonadPlus должны подчиняться, законы тождества и ассоциативности (a.k.a. моноидные законы):

Я не уверен, что был проведен опрос. В Докладе нет законов для mplus (возможно, авторы все еще обсуждали их). Так что я сказал бы, что проблема открыта - и это главное послание в поперечнике.

Ответ 3

Редко, что экземпляры MonadPlus нарушают ассоциативность, но явно не невозможны. Typeclasses можно пересчитать только для удовлетворения "очевидных" законов до определенной суммы. Например, четыре дополнительных набора возможных законов для MonadPlus обсуждаются здесь без каких-либо выводов и с библиотеками, следующих за различными соглашениями, без указания того, какой из них.

Ясно, что у Олега есть причина отклонить ассоциативность. Является ли это "действительно экземпляром MonadPlus"? Кто знает, это недостаточно хорошо, чтобы сказать.