*To*: Martin Desharnais <martin.desharnais at gmail.com>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Why is Monad_Syntax.bind right and not left associative?*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Fri, 26 Jul 2019 14:56:15 +0200*In-reply-to*: <577a11a0-ed58-193a-7f62-7e156f0a4712@gmail.com>*References*: <577a11a0-ed58-193a-7f62-7e156f0a4712@gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:60.0) Gecko/20100101 Thunderbird/60.8.0

Am 26.07.2019 um 14:12 schrieb Martin Desharnais: > 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? I just had a look at the history: - Originally (2008), the heap monad in Imperative HOL was left-associative (cf. https://isabelle.in.tum.de/repos/isabelle/annotate/66e6b967ccf1/src/HOL/Library/Heap_Monad.thy#l63). IIRC, this was the first serious use of monads in Isabelle/HOL. - The generic Monad_Syntax was introduced later (in 2010), and it was right-associative (cf. https://isabelle.in.tum.de/repos/isabelle/annotate/7fea92005066/src/HOL/Library/Monad_Syntax.thy#l12). I do not remember any specific technical reason for it, except maybe that expressions arising from do-notation would typically associate to the right (with lambdas). But it may well have been an accident. One could think about changing this, to conform to Haskell (but with possible impact on many theories). Heavy monad users: Please comment! Alex

**Follow-Ups**:**Re: [isabelle] Why is Monad_Syntax.bind right and not left associative?***From:*Klein, Gerwin (Data61, Kensington NSW)

**References**:**[isabelle] Why is Monad_Syntax.bind right and not left associative?***From:*Martin Desharnais

- Previous by Date: [isabelle] Why is Monad_Syntax.bind right and not left associative?
- Next by Date: [isabelle] Things identified via `rewrites` not treated as identical
- Previous by Thread: [isabelle] Why is Monad_Syntax.bind right and not left associative?
- 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