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



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




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