Email Gateway (Sep 29 2022 at 10:43): Email Gateway (Sep 29 2022 at 10:43):From: Peter Lammich <lammich@in.tum.de>
Where's the syntactic signed_division type class gone.
I remember that it was a convention to have syntactic type-classes that
define the operators, and make no assumptions.
This used to be the case for signed_division
(HOL-Library.Signed_Division), but has changed now, and the sdiv and
smod are defined only in a typeclass with assumptions.
This breaks my formalization, with the only workarounds being to use
different infix operators, or to hide and overload the ones defined by
signed-division
... both inferior solutions to simply using sdiv/smod to express signed
division (however in a type where it's only partially defined, and thus
does not satisfy the class assumptions)
Any particular reason for that change? Or just by accident?
Email Gateway (Oct 01 2022 at 08:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter et. al.,
for the moment being it is not a big deal to introduce dedicated
syntactic type classes for _ sdiv _ and _ smod _.
A change is underway, but I have to await the test results of that and a
predecessor; this will hopefully happen during today, otherways I will
send a dedicated change to Makarius.
The state-of-the-art device for managing reusable syntax are bundles,
and some examples can now be found in the distribution, notably the
infix bit operations. Their applications still requires boilerplate,
and I would definitely not suggest to use them for pervasive syntax like
More instances of that pattern will bring suggestions what is needed to
make it even more convenient. (think loudly – sth. like default bundles
scoped to a theory could be an idea).
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature
Email Gateway (Oct 01 2022 at 09:17):From: Peter Lammich <lammich@in.tum.de>
Hi Florian.
A change is underway,
great!
The state-of-the-art device for managing reusable syntax are bundles,
and some examples can now be found in the distribution, notably the
infix bit operations. Their applications still requires boilerplate,
and I would definitely not suggest to use them for pervasive syntax
like + * - at the moment, but for more exotic notations everything
should work out fine already.
They have the disadvantage that you cannot have multiple bundles with
the same syntax unbundled.
In my case, I am working with lemmas of the form:
bitsize a = bitsize b ==> a sdiv b = to_int a sdiv to_int b
you could argue that this dual use of sdiv, as partial function and as
total function, might be confusing, and you should introduce another
name. But that's a design decision, and depends on many factors. Not
having a syntactic type-class forces this decision one way.
And, similarly, for other theories (I use regularly), e.g.,
Separation_Algebra, where + is overloaded to have partial meaning.
Also an opinion: sdiv and smod being one of the basic operations on
words, I do not consider them particularly 'exotic'.
Email Gateway (Oct 02 2022 at 13:45):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
They have the disadvantage that you cannot have multiple bundles with
the same syntax unbundled.
That's right. We have no syntactic overloading yet. Until them, we have
to work with funny combinations of lettes and glyphs.
Also an opinion: sdiv and smod being one of the basic operations on
words, I do not consider them particularly 'exotic'.
With »exotic« I mean not the the operations are »uncanonical« but are
not pervasively used in arbitrary theories like e. g. addition.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature
Email Gateway (Oct 03 2022 at 07:06):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi Florian,
The state-of-the-art device for managing reusable syntax are bundles,
and some examples can now be found in the distribution, notably the
infix bit operations. Their applications still requires boilerplate,
and I would definitely not suggest to use them for pervasive syntax
like + * - at the moment, but for more exotic notations everything
should work out fine already.
I'd like to stress that "syntactic type classes" are not purely useful
for input syntax but can have useful logical implications related to
type-classes.
As a slightly contrived example:
Assume we write a new type class "ordered_enum".
Which has the axioms:
enum_ordered: "forall x,y: x <= y ==> exists i,j with i <= j: enum!i
= x /\ enum!j = y" (basically: enum is an ordered list of all elements
of the type)
enum_unique: "unique enum" (no duplicates)
If there were a syntactic type class for enum, I could write
class ordered_enum = linorder + *syntactic_enum *+ assumes
enum_ordered: "...." and enum_unique: "...."
and then later prove "subclass ordered_enum <= enum" (because the enum
axioms easily follow from the stronger ones given here).
But since we do not have a syntactic enum, we have to write (as far as I
can tell):
class ordered_enum = linorder + *enum *+ assumes enum_ordered:
"...." and enum_unique: "...."
This gives the same effect in the end, except that now in every instance
proof of ordered_enum, we need to additionally prove the enum axioms.
This increases redundancy unnecessarily.
Even more problematic is when someone wants to introduce additional
typeclasses that have less requirements than the existing ones. Imagine
the syntactic "ord" would not exist (i.e., "order" would be the first
type class defining less_eq), then it would not be possible to introduce
a type-class quasiorder that, say, does not have antisymmetry. (Or, it
would be possible, but it would be impossible to make it a superclass of
"order".)
So I would advocate keeping the syntactic classes even if fancy syntax
extensions become possible in the future.
Best wishes,
Dominique.
More instances of that pattern will bring suggestions what is needed
to make it even more convenient. (think loudly – sth. like default
bundles scoped to a theory could be an idea).Cheers,
FlorianAm 29.09.22 um 12:43 schrieb Peter Lammich:
Where's the syntactic signed_division type class gone.
I remember that it was a convention to have syntactic type-classes
that define the operators, and make no assumptions.This used to be the case for signed_division
(HOL-Library.Signed_Division), but has changed now, and the sdiv and
smod are defined only in a typeclass with assumptions.This breaks my formalization, with the only workarounds being to use
different infix operators, or to hide and overload the ones defined
by signed-division... both inferior solutions to simply using sdiv/smod to express
signed division (however in a type where it's only partially defined,
and thus does not satisfy the class assumptions)Any particular reason for that change? Or just by accident?
--
Peter
On 18/09/2022 16:04, Makarius wrote:
Dear Isabelle users,
we are making quick progress with the Isabelle2022, which is to be
finalized until 23-Oct-2022.The release process is continuously documented on the blog entry
https://isabelle-dev.sketis.net/phame/post/view/58/release_candidates_for_isabelle2022
--- this includes a list of notable changes.The current release candidate is
https://isabelle.sketis.net/website-Isabelle2022-RC2A corresponding version of the Archive of Formal Proofs is
https://isabelle.sketis.net/repos/afp-devel/rev/34a31d29f666.Any feedback about Isabelle release candidates should be posted with
a meaningful Subject (not just a clone of the announcement).Makarius
Email Gateway (Oct 06 2022 at 12:28):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dominique,
I'd like to stress that "syntactic type classes" are not purely useful
for input syntax but can have useful logical implications related to
type-classes.
I did not stress that issue in my last e-mail, but I am aware of this
– one concrete example requiring the same pattern in the distribution is
»gcd«.
So I would advocate keeping the syntactic classes even if fancy syntax
extensions become possible in the future.
I don't think that there will be even the chance of any massive movement in
the distribution to abolish syntactic type classes.
On the other side I don't think it is a good idea to introduce syntactic
type classes unconditionally, but follow an on-demand approach here.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature
Last updated: Apr 26 2024 at 04:17 UTC