Email Gateway (Feb 10 2021 at 15:07): Email Gateway (Feb 10 2021 at 15:07):From: Manuel Eberl <eberlm@in.tum.de>
Hello,
there is a Haskell extension that allows writing nested ifs in the
following nice syntax:
if | P -> a
| Q -> b
| R -> c
| otherwise -> d
I asked around and some people (e.g. Tobias Nipkow) agree that this
might be nice to have. My proposed syntax is inspired by the "case"
syntax and looks like this:
if P ⇒ x | Q ⇒ y | R ⇒ z | otherwise ⇒ u
One could also do
if P ⇒ x | Q ⇒ y | R ⇒ z | _ ⇒ u
instead.
I attached a small theory that implements this.
Not sure if this should be enabled for output by default as well –
probably not. One could switch it on only in a special "multi_if" print
mode, similarly to "do_notation" for monad syntax.
The current implementation has the problem that "if b then x else y"
gets output as "if b ⇒ x | otherwise ⇒ y", which we clearly don't want.
Not sure how to fix that.
Manuel
Multiway_If.thy
smime.p7s
Email Gateway (Feb 10 2021 at 15:41):From: Peter Lammich <lammich@in.tum.de>
Maybe could go to HOL-Library ?
Email Gateway (Feb 10 2021 at 15:54):From: Manuel Eberl <eberlm@in.tum.de>
It could, but I for one think something like this should either be
enabled by default or not exist at all (at least as input syntax – as
output, it is debatable).
Manuel
smime.p7s
Email Gateway (Feb 10 2021 at 18:59):From: Christian Sternagel <c.sternagel@gmail.com>
On 2/10/21 4:07 PM, Manuel Eberl wrote:
Hello,
there is a Haskell extension that allows writing nested ifs in the
following nice syntax:if | P -> a
| Q -> b
| R -> c
| otherwise -> dI asked around and some people (e.g. Tobias Nipkow) agree that this
might be nice to have. My proposed syntax is inspired by the "case"
syntax and looks like this:if P ⇒ x | Q ⇒ y | R ⇒ z | otherwise ⇒ u
One could also do
if P ⇒ x | Q ⇒ y | R ⇒ z | _ ⇒ u
instead.
I attached a small theory that implements this.
Not sure if this should be enabled for output by default as well –
probably not. One could switch it on only in a special "multi_if" print
mode, similarly to "do_notation" for monad syntax.The current implementation has the problem that "if b then x else y"
gets output as "if b ⇒ x | otherwise ⇒ y", which we clearly don't want.
Not sure how to fix that.
Dear Manuel,
Naive question: What if you would use your own dedicated constant
definition "multi_if == If"
together with some suitable simplification rules and/or other automation?
Then users could decide on their own which syntax to use (for input and
output).
cheers
chris
Manuel
Email Gateway (Feb 10 2021 at 19:03):From: Manuel Eberl <eberlm@in.tum.de>
One could of course do that. I'm not really sure it's better. I think I
would prefer having it just as notation. But I'm not opposed to it either.
Manuel
smime.p7s
Email Gateway (Feb 10 2021 at 21:38):From: Gerwin Klein <kleing@unsw.edu.au>
I'd be against introducing another If definition. There is a lot of automation that interacts with "If", and if you maintain your own automation, you'd now have to do two sets.
Not opposed to the notation, though. If we can figure out a way to not fire for single "if P => x | otherwise => y" case that could be quite nice. It could be part of the standard If as input, and as a bundle for output.
Cheers,
Gerwin
signature.asc
Email Gateway (Feb 19 2021 at 15:20):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Manuel Eberl/All,
Incidentally, I am working on a theory that could greatly benefit from the
use of a multiway if. Given that it is not part of the standard, I am
wondering if there already exist any (third-party) alternatives to this
notation. If not, technically, if I was to (outright) copy a part of a post
on the mailing list into my own library, I believe, I would be violating
copyright laws (please correct me, if I am wrong). Thus, I have to ask you
for explicit permission to reuse this code. Also, what kind of
attribution/license would such reuse require (provided, of course, that you
can grant permission)?
Kind Regards,
Mikhail Chekhov
Email Gateway (Feb 19 2021 at 15:37):From: Manuel Eberl <eberlm@in.tum.de>
Hello,
feel free to use whatever you want from me. You can put a short comment
like "contributed by Manuel Eberl, see mailing list post <url>" or
something like that, but you don't have to – it's not a big thing and I
don't need to get attribution for it. :)
Since there seems to be a consensus that this would be nice to have, I
will probably put something like this into the distribution before the
next release anyway though. I would already have done it, had it not
been for the somewhat annoying issue of getting the output right.
Manuel
smime.p7s
Last updated: Apr 24 2024 at 16:18 UTC