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



Just as another data point: I also don't remember any specific reasons
for >>= being infixr.

And, like sel4, in IsaFoR we mostly use do-notation (683 occurrences)
over explicit binds (20 occurrences).

cheers

chris

On 7/28/19 3:09 AM, Klein, Gerwin (Data61, Kensington NSW) wrote:
> 
> 
>> On 26 Jul 2019, at 22:56, Alexander Krauss <krauss at in.tum.de> wrote:
>>
>> 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.
> 
> I would say monad use in Isabelle goes back to at least 2005 in the seL4 proofs, it was just not part of the Isabelle repo. Our main bind operator is left associative like in Haskell.
> 
> 
>> - 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!
> 
> We do use the generic monad syntax heavily in the newer parts of the seL4, but I didn’t even notice that the generic bind was declared infixr, because we mostly directly use do-notation, so I would expect a fairly low impact for that change at least on us.
> 
> Cheers,
> Gerwin
> 




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