Email Gateway (Aug 23 2022 at 09:26): Email Gateway (Aug 23 2022 at 09:26):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Hi,
when using records a common theme is to just update some fields of a
record and leave the others at is. To this end, many functional
languages have a record update syntax, e.g. in OCaml you can write {bar
with x = 1} to obtain a new record that has all the same values as bar
except for x. As far as I can see, Isabelle/ML currently has no such
syntax which can lead to quite a bit of bloat. For a pathological
example, see src/Provers/order.ML where multiple functions are declared
that each just update one field of the record, but you still have to
explicitly provide all the other fields. It would be nice to have this
build into the language. An even more flexible solution would be to
implement this as an ML antiquotation; however, this requires the
ability to introspect the type of a record to obtain a list of all the
record members. I am not sure if this is currently (or at all) possible.
Is there any interest in having such a language construct?
Lukas
Email Gateway (Aug 23 2022 at 09:26):From: Makarius <makarius@sketis.net>
On 28/07/2020 12:39, Lukas Stevens wrote:
when using records a common theme is to just update some fields of a record
and leave the others at is. To this end, many functional languages have a
record update syntax, e.g. in OCaml you can write {bar with x = 1} to obtain a
new record that has all the same values as bar except for x. As far as I can
see, Isabelle/ML currently has no such syntax which can lead to quite a bit of
bloat.
The bloat is not just in the syntax, but also in the implementation: a bulky
record needs to be copied to change just one field.
Further note that record update is not as exciting as it seems. More important
is the "map" combinator for each individual field. The pair of (selector, map)
is called a "lense" in Haskell context (but we can work with it directly in
Isabelle/ML without the categorical overhead around it, and just compose
combinators via infix "o").
Here is a canonical example to cope reasonably well in the absence of
compiler-generated record operations:
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/variable.ML#l104
Another possibility to trim down complexity of syntax (and runtime behaviour)
is to nest records/tuples in stages. E.g. see
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/context.ML#l141
Yet another variant is to use tuples, i.e. records with fields named 1, 2, 3,
... and use the Isabelle/ML antiquotations to inline map combinators like
@{apply (3)1}, e.g. see
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/Tools/generated_files.ML#l60
For a pathological example, see src/Provers/order.ML where multiple>
functions are declared that each just update one field of the record, but you
still have to explicitly provide all the other fields.
That merely looks like an odd example, so it is better not to imitate it. When
inspecting existing material, you need to develop a feeling who did it at
which time, and estimate how well it was actually done.
The "order" prover is from an undergraduate student project from many years
ago. It looks like the source text could be deflated a lot, by making it more
"canonical" in terms of Isabelle/ML style and orthography.
(MoreoverIsabelleSourcesDoNotUseCamelCaseToImproveReadability.)
The somewhat awkward type less_arith with its many homogenous fields could be
just a table that maps a rule name (type string) to a rule (type thm). See our
bread-and-butter module Pure/src/General/table.ML
An alternative is to use a 19-tuple and the @{apply} antiquotation.
It would be nice to
have this build into the language. An even more flexible solution would be to
implement this as an ML antiquotation; however, this requires the ability to
introspect the type of a record to obtain a list of all the record members. I
am not sure if this is currently (or at all) possible.Is there any interest in having such a language construct?
"Nice to have" is often a bad reason to add new features. Languages tend to
accumulate a lot of cruft over the years, and after some decades the
"must-haves" from the past become a heavy burden. (OCaml has a lot of that
with its object-oriented twists.)
Isabelle/ML has its own balance of frugality and richness, both in the same
language. The rather ancient SML substrate works surprisingly well with the
minor add-ons provided Isabelle/ML.
I often find the balance of Isabelle/ML better than Scala, which has many good
ideas, but also tons of extra weight and gravity to bog it down. In
particular, Scala "cases classes" with their record-update notation ("copy"
method) are not as smooth as they should be.
Makarius
Email Gateway (Aug 23 2022 at 09:27):From: "Norrish, Michael (Data61, Acton)" <Michael.Norrish@data61.csiro.au>
See also
http://mlton.org/FunctionalRecordUpdate
for an SML solution, of sorts.
Michael
On 29/7/20, 06:23, "cl-isabelle-users-bounces@lists.cam.ac.uk on behalf of Makarius" <cl-isabelle-users-bounces@lists.cam.ac.uk on behalf of makarius@sketis.net> wrote:
On 28/07/2020 12:39, Lukas Stevens wrote:
when using records a common theme is to just update some fields of a record
and leave the others at is. To this end, many functional languages have a
record update syntax, e.g. in OCaml you can write {bar with x = 1} to obtain a
new record that has all the same values as bar except for x. As far as I can
see, Isabelle/ML currently has no such syntax which can lead to quite a bit of
bloat.
The bloat is not just in the syntax, but also in the implementation: a bulky
record needs to be copied to change just one field.
Further note that record update is not as exciting as it seems. More important
is the "map" combinator for each individual field. The pair of (selector, map)
is called a "lense" in Haskell context (but we can work with it directly in
Isabelle/ML without the categorical overhead around it, and just compose
combinators via infix "o").
Here is a canonical example to cope reasonably well in the absence of
compiler-generated record operations:
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/variable.ML#l104
Another possibility to trim down complexity of syntax (and runtime behaviour)
is to nest records/tuples in stages. E.g. see
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/context.ML#l141
Yet another variant is to use tuples, i.e. records with fields named 1, 2, 3,
... and use the Isabelle/ML antiquotations to inline map combinators like
@{apply (3)1}, e.g. see
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/Tools/generated_files.ML#l60
For a pathological example, see src/Provers/order.ML where multiple>
functions are declared that each just update one field of the record, but you
still have to explicitly provide all the other fields.
That merely looks like an odd example, so it is better not to imitate it. When
inspecting existing material, you need to develop a feeling who did it at
which time, and estimate how well it was actually done.
The "order" prover is from an undergraduate student project from many years
ago. It looks like the source text could be deflated a lot, by making it more
"canonical" in terms of Isabelle/ML style and orthography.
(MoreoverIsabelleSourcesDoNotUseCamelCaseToImproveReadability.)
The somewhat awkward type less_arith with its many homogenous fields could be
just a table that maps a rule name (type string) to a rule (type thm). See our
bread-and-butter module Pure/src/General/table.ML
An alternative is to use a 19-tuple and the @{apply} antiquotation.
It would be nice to
have this build into the language. An even more flexible solution would be to
implement this as an ML antiquotation; however, this requires the ability to
introspect the type of a record to obtain a list of all the record members. I
am not sure if this is currently (or at all) possible.Is there any interest in having such a language construct?
"Nice to have" is often a bad reason to add new features. Languages tend to
accumulate a lot of cruft over the years, and after some decades the
"must-haves" from the past become a heavy burden. (OCaml has a lot of that
with its object-oriented twists.)
Isabelle/ML has its own balance of frugality and richness, both in the same
language. The rather ancient SML substrate works surprisingly well with the
minor add-ons provided Isabelle/ML.
I often find the balance of Isabelle/ML better than Scala, which has many good
ideas, but also tons of extra weight and gravity to bog it down. In
particular, Scala "cases classes" with their record-update notation ("copy"
method) are not as smooth as they should be.
Makarius
Email Gateway (Aug 23 2022 at 09:27):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Thanks for the answer and the additional practical hints.
Of course, the example is, as I said, pathological but you will find
clumsy usage of records in other places as well.
I agree with you that introducing a new language feature would not be a
good idea. Lenses would probably be a nice and flexible solution. The
problem with those is that you have to write quite a bit of boilerplate
if you can't generate them automatically. To generate them
automatically, one could define an ML antiquotation that reads a record
type definition and defines the record type while automatically
generating the code for the lens as well. Or is there a way to generate
the lens for an existing record type (which would make it more flexible)?
Last updated: Apr 26 2024 at 12:28 UTC