Email Gateway (Feb 10 2023 at 13:09): Email Gateway (Feb 10 2023 at 13:09):From: Tobias Nipkow <nipkow@in.tum.de>
There is an awful lot of special purpose syntax (eg "f(x |-> y)" instead of "f(x
:= Some y)") declared in the theory Map which is part of Main. I would like to
get rid of most if not all of it (by default, but with ways of including it). If
you think it is a good or a bad idea, voice your opinion here. If you would like
to be included in a separate discussion of what to remove and how, let me know
(possibly by a private email).
Tobias
Email Gateway (Feb 11 2023 at 09:19):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Tobias,
just a thought from a decade ago:
The only operation which is used pervasively seems to be map_of
(I have found no notes but I remember quite confidently that this was
the result of a closer analysis); map_of could be separated (e. g. going
to List.thy) and Map.thy moved to HOL-Library.
There are alternatives to map_of for constructing functions from
explicit key-value-tables, but that is a different story.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature
Email Gateway (Feb 11 2023 at 10:58):From: "C. Diekmann" <diekmann@net.in.tum.de>
Hi Tobias,
To be honest, I like the map syntax with |-> very much. This includes the
following:
Map update: m(x |-> y)
Map update multiple: m(x1 |-> y1, x2 |-> y2, ...)
Map initialization: [ x1 |-> y1, x2 |-> y2, ... ]
Having this syntax helps me during modeling when dealing with data.
And it looks super nice to write down some initial examples this way.
Having maps as a first class citizen in the standard lib with nice syntax
also helps me to pick them whenever I need a finite data store. It's always
hard to overcome my initial resistance when I know I want some storage-like
object like a list or a dictionary to pick the least intuitive data
structure: a partial function. But this usually turns out to be the right
choice. And having some nice syntax along the way really helps me to feel
that I'm modelling stuff correctly here.
So I really like all the |-> syntax, even though := Some would do the
same. Technically, the |-> syntax provides little value, but for me
personally, this syntax has enormous *mental *value, since it helps me to
do the *mental *lifting to pick a partial function when I'm actually
looking for a dictionary-like data structure.
Anecdotally, at least for me, very often, it turns out later that I
actually don't need a partial function at all and modelling things with a
normal function makes the whole theory simpler. That's why I probably use
the |-> syntax less during later stages of development or even get rid
of it. And I probably never used any of the other map syntax, like map
composition or map subset. Those can go away. But, at least for me, the |->
syntax should remain to help with the mental transition from data to
function.
I hope this helps. I just had some years where I barely used Isabelle, but
I started again recently. Since I was somehow out of practice, I tried to
look very closely at what kinds of mistakes I make or where I get stuck.
And dealing with data in Isabelle models was one of those and
re-discovering the concepts of maps really unblocked me there.
Cheers,
Cornelius
Email Gateway (Feb 11 2023 at 16:44):From: Makarius <makarius@sketis.net>
Just a technical side-remark: In the past decades we often found changes of
mixfix syntax infeasible, such that historic notation often got stuck for no
particular reason. Most ASCII replacement syntax falls into this category,
e.g. "x : A" instead of "x \<in> A" (and all its derivative forms).
Now the we have an improved "isabelle update" tool that scales to all of
Isabelle + AFP and has access to PIDE markup to guide the replacement. E.g.
see this spot in the Isabelle repository
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Pure/Tools/update.scala;9107e103754c$14
It is a bit of an art to find correct and complete XML markup tree structure
for particular update tasks, but it usually works.
There is no general scheme for mixfix syntax yet. E.g. there could be an
update specification as part of the normal syntax for mixfix annotations,
which the "isabelle update" tool will use accordingly. One day this will be
available, but not now.
Concerning the spring cleaning of theory HOL.Map, this is merely an
encouragement to be more bold and ambitious than usual in fresh ideas.
Afterwards, we can see if and how to update all existing sources, while
avoiding the infamous "SOMEthing went utterly wrong" problem --- wild
replacements in plain text without a formal context.
Makarius
Email Gateway (Feb 13 2023 at 10:23):From: Tobias Nipkow <nipkow@in.tum.de>
Cornelius,
Thanks for your feedback. I had not planned to get rid of the |-> syntax
completely but at most to make it optional. Now it looks like you would only
have to import Map explicitly.
Tobias
Email Gateway (Feb 13 2023 at 10:25):From: Tobias Nipkow <nipkow@in.tum.de>
Florian,
That seems like a plan: move map_of to List and Map.thy to Library.
Thanks
Tobias
Email Gateway (Feb 21 2023 at 14:40):From: Tobias Nipkow <nipkow@in.tum.de>
It turns out that practically all Map operators and syntax are used widely
enough that it is better to leave things as they are. With the exception of some
clumsy ASCII syntax. One could get rid of
|` for the symbol \<restriction>
|-> for the symbol \<mapsto>
However, I am not an expert for udate tools and leave this to somebody who is ;-)
Tobias
Last updated: Apr 19 2024 at 12:27 UTC