Re: [isabelle] Why is Monad_Syntax.bind right and not left associative?
- To: Alexander Krauss <krauss at in.tum.de>
- Subject: Re: [isabelle] Why is Monad_Syntax.bind right and not left associative?
- From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein at data61.csiro.au>
- Date: Sun, 28 Jul 2019 01:09:20 +0000
- Accept-language: en-AU, en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1;spf=pass smtp.mailfrom=data61.csiro.au;dmarc=pass action=none header.from=data61.csiro.au; dkim=pass header.d=data61.csiro.au; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=jGevSvKW7pUMs4zpdd94CFltKwftUjnhp4s45GlK7/U=; b=k9xM2ayAxkV/buv6RKnjxVkaG6iCfhzxLLeE3imJvt5Kj2PCX5kSnFkByKe2kYqtBp0GFaOxczjthCwGG9npYOwgLP431lI547SpB9Wfha7R5aoh+FP1D3ckbBXa6+58fNUIZjXjSec967PHtYhRoWuEwAjMkmMuKetQMtNb5KlD1VcdUUg5qucSBZ67cjLpRSBnAUa3WxRCXbX5cNel19mmn2gSMoHykeMQH8+HfyfSyNTUjumSNRFYBT3WxnQnsJseIIKms2lOuo8jccJh4Rp1JQNmMnijHO7jh1Tvr2NDuHV1Yvdoru1XhDe7icZTnZaTNNLFwvYTzrmC5Dv0qw==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=Yd0jZ168uhUsvZkAeCafxYWJOXBfDbqErnVRzpr/B0FVYyqo4V6C60ODU4X5t+FdFbqFaDQnuTeQiwpfscus4S34/SbEzpeaGijL27MdFzFnykkWwetqZykGA6FldpYeGKAB6qCtrtvypV0Wj4KzjYWetbJdkw1AAYVsIOr1BsgOiS2iZkr+Ry1DP3oPcotRVi3Mh4H84wu0duIr9EYi8RbDBHvs1kYdBmTgi0sJkyxhWc/r3ACqazZO0tAc9RNZqxLqB2RWHP5/torZ9DRCW9qigl4mXrp+RBDOrkU3Xv1LxoFGZN9N/lp2oGS5ZFyyctcdH1E/iV6jtQWOABoosQ==
- Authentication-results: spf=none (sender IP is ) smtp.mailfrom=Gerwin.Klein at data61.csiro.au;
- Cc: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>, Martin Desharnais <martin.desharnais at gmail.com>
- In-reply-to: <email@example.com>
- Ironport-phdr: 9a23:mWhM7RABJ1HuYxofbZzQUyQJPHJ1sqjoPgMT9pssgq5PdaLm5Zn5IUjD/qo03kTRU9Dd7PRJw6rNvqbsVHZIwK7JsWtKMfkuHwQAld1QmgUhBMCfDkiuA/PwcC08WudGWV5j132yLUELQYD1fFzIpTu78G1aFw==
- Ironport-sdr: 4E7eQz4fqmaJUIZelqKNhYEUS7+4W10HETk15gAEcWG7Zl6yVM5nU0GRK4VGlCUZU42tQwZfzp qtJiP3uWlmuA==
- References: <firstname.lastname@example.org> <email@example.com>
- Thread-index: AQHVQ7HpM5eDW5s4HU6AN5K3tfq6zKbfOsaA
- Thread-topic: [isabelle] Why is Monad_Syntax.bind right and not left associative?
> 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.
> 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.
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and