Dear Martin,We have made "bind" left-associative now, which is customary and makes more sense. Thank you for notifying us.
Tobias On 26/07/2019 14:12, Martin Desharnais wrote:
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 bindI 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 operands. theory Scratch imports Main "HOL-Library.Monad_Syntax" begin context fixes f :: "nat ⇒ 'a ⇒ 'a option" and x :: "'a" begin 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)" *) end end 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
Description: S/MIME Cryptographic Signature