*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Why is Monad_Syntax.bind right and not left associative?*From*: Martin Desharnais <martin.desharnais at gmail.com>*Date*: Fri, 26 Jul 2019 14:12:10 +0200*Autocrypt*: addr=martin.desharnais at gmail.com; prefer-encrypt=mutual; keydata= mDMEWeXYxRYJKwYBBAHaRw8BAQdAsOV1c6NtNeZBj4FQWywoTTKNwQNx8oCLJOQtQXKx/Ku0 L01hcnRpbiBEZXNoYXJuYWlzIDxtYXJ0aW4uZGVzaGFybmFpc0BnbWFpbC5jb20+iJYEExYI AD4WIQSQsb+oyQIj1XPAsM96+p9h8fpD5gUCWeXYxQIbAwUJCWYBgAULCQgHAgYVCAkKCwIE FgIDAQIeAQIXgAAKCRB6+p9h8fpD5hVIAQDQsCvKjL3JErp33GHs+PdD1gUIdPCG50Crsbrd 5zNVmAEAwadxF17qkhcAXcqr2galgofB4rYEp8HmJO+sXj2KJwe4OARZ5djFEgorBgEEAZdV AQUBAQdAojxcR37buaV6a1MGo/O19BAixUlmCNccrH8Uab+L+kkDAQgHiH4EGBYIACYWIQSQ sb+oyQIj1XPAsM96+p9h8fpD5gUCWeXYxQIbDAUJCWYBgAAKCRB6+p9h8fpD5m8RAQDb4yBL kq0ZjR6Jl4vHsz0wF5SosX96To4vlzucTQq/RwD/SgY4mEUbKq7e4s/YT/jUJMUcGf+UCWUS z11mIqDZdAU=*Openpgp*: preference=signencrypt*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.8.0

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 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

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Why is Monad_Syntax.bind right and not left associative?***From:*Alexander Krauss

**Re: [isabelle] Why is Monad_Syntax.bind right and not left associative?***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Question about Axiom specification
- Next by Date: Re: [isabelle] Why is Monad_Syntax.bind right and not left associative?
- Previous by Thread: Re: [isabelle] Question about Axiom specification
- Next by Thread: Re: [isabelle] Why is Monad_Syntax.bind right and not left associative?
- Cl-isabelle-users July 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list