[isabelle] Why is Monad_Syntax.bind right and not left associative?

Dear Isabelle users,

I recently discovered the `HOL-Library.Monad_Syntax` theory with its
(>>=) and do-notation. While defining an inductive predicate using
multiple bind operations, I encountered the following error message.

> Unresolved adhoc overloading of constant bind

I minimized the my code until I noticed that the error only occurs with
two or more binds and can be resolved by adding parenthesis on the left

theory Scratch
  imports Main "HOL-Library.Monad_Syntax"

  fixes f :: "nat ⇒ 'a ⇒ 'a option" and x :: "'a"

declare [[show_variants]]

term "Some x >>= f 0"
(* "Option.bind (Some x) (f 0)" :: "'a option" *)

term "Some x >>= f 0 >>= f 1"
(* Unresolved adhoc overloading of constant bind *)

term "((Some x) >>= f 0) >>= f 1"
(* "Option.bind (Option.bind (Some x) (f 0)) (f 1)" *)



I checked the source code of `Monad_Syntax` and noticed that it is
declared as `infixr ">>=" 54`. I was quite surprised because such a
choice requires one to add extra parenthesis in what seem to be common
cases and the traditional Haskell (>>=) operator itself is left associative.

What is the reasoning for the Isabelle (>>=) to be right and not left
associative? What are situations where it makes more sense?

Best regards,
Martin Desharnais

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.