Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Record update syntax


view this post on Zulip Email Gateway (Jul 28 2020 at 10:39):

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

view this post on Zulip Email Gateway (Jul 28 2020 at 20:21):

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

view this post on Zulip Email Gateway (Jul 28 2020 at 23:08):

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

view this post on Zulip Email Gateway (Jul 31 2020 at 10:20):

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)?

view this post on Zulip Email Gateway (Aug 03 2020 at 12:00):

From: Makarius <makarius@sketis.net>
On 31/07/2020 12:19, Lukas Stevens wrote:

Of course, the example is, as I said, pathological but you will find
clumsy usage of records in other places as well.

What is your own application like? Is it more like the 19-tuple in
src/Provers/order.ML or like the 8-tuple in src/Pure/variable.ML (or even less
complex)?

I do see slight inconveniences in using records in SML and thus Isabelle/ML,
but the overall balance is still quite good (compared to related or unrelated
inconveniences in Scala, Haskell, OCaml).

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)?

In the meantime I have also spent more thoughts on the general problem of
records in SML.

I don't want to see genuine language extensions: this would further weaken the
language and its few implementations. SML is de-facto a dead language (like
classical Latin), and hypothetical discussions and proposals like
https://smlfamily.github.io/successor-ml are not going to change that after
several decades.

I also don't want to see fancy workarounds like in MLton
http://mlton.org/FunctionalRecordUpdate --- that is a somewhat different
culture from Isabelle/ML. Why make a relatively simple problem harder than it
really is?

Nonetheless, I see a prospect of future refinements of Isabelle/ML as follows:

* The very essence of a record in SML is the list (or set) of fields, not
the concrete field types. Field names are global, without scope, but field
types are determined by type-inference in a particular scope of ML text.

* There could be an antiquotation @{record RECORD = FIELDS ...} to define a
named set of fields within the Isabelle/ML compiler context.

* The existing antiquotation @{apply m(n)} could be generalized to @{apply
RECORD(FIELD)}.

* There could be a few more antiquotations, e.g. @{make RECORD} for a
function that composes a record from its fields.

Makarius

view this post on Zulip Email Gateway (Aug 03 2020 at 12:38):

From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
The application is exactly src/Provers/order.ML but I'd like to refactor
the interface of the prover to reduce boilerplate on the ML side of
things. Reducing boilerplate when instantiating the prover would also be
great. One way is, as you suggested, to just use tables instead of
records. This would increase the opaqueness of the code since it hides
which theorems are needed exactly. Another way would be to use the
antiquotations you proposed. Especially the generalised antiquotation
would be great and also make sense since records can be viewed as tuples
with names instead of indices.

view this post on Zulip Email Gateway (Aug 03 2020 at 13:18):

From: Makarius <makarius@sketis.net>
On 03/08/2020 14:38, Lukas Stevens wrote:

The application is exactly src/Provers/order.ML but I'd like to refactor
the interface of the prover to reduce boilerplate on the ML side of
things. Reducing boilerplate when instantiating the prover would also be
great. One way is, as you suggested, to just use tables instead of
records. This would increase the opaqueness of the code since it hides
which theorems are needed exactly.

In that case, I do propose to use a plain table that maps a thm name to thm
value: the Order_Tac module has already several operations that use (untyped)
string "tags" instead of typed record fields, so it fits stylistically and
actually simplifies the current situation (notably operations like "empty" and
"update"; the odd dummy_thm will disappear, it is replaced by an undefined
table entry).

As you proceed to explore order.ML and learn idiomatic use of Isabelle/ML, you
will find more and more ways to make the implementation concise and to the point.

(The file name should be actually order_tac.ML in correspondence to structure
Order_Tac in it.)

There is yet another perspective on the problem: type less_arith is like an
algebraic structure with "laws" for operations (=), (<=), (<). This could in
principle become an axiomatic specification as a locale context, and the tool
then operates "under a morphisms" to move it from the abstract context to
application contexts.

Then the record disappears altogether and is replaced by fancy operations on
logical context elements (due to locale interpretation). An example for this
approach is src/HOL/Tools/semiring_normalizer.ML but it has its own added
complexity.

Another way would be to use the
antiquotations you proposed. Especially the generalised antiquotation
would be great and also make sense since records can be viewed as tuples
with names instead of indices.

Right now I recommend to concentrate on the core problems of the application,
and ignore accidental inconveniences of records in Isabelle/ML.

Makarius

view this post on Zulip Email Gateway (Aug 03 2020 at 14:14):

From: Thomas Sewell <sewell@chalmers.se>
Excuse me. I haven't read all the emails in this discussion, but it doesn't look like anyone has

pointed out the fact that the Isabelle equivalent of caml-style

{bar with x = 1}

is

(bar (| x := 1 |) )

The constant below the syntax is called x_update. Apologies if someone has said this and I missed it.

There is no equivalent of row-typing, so there's no way to do this polymorphically across all records that have an x field.

Best regards,

Thomas.


From: cl-isabelle-users-bounces@lists.cam.ac.uk <cl-isabelle-users-bounces@lists.cam.ac.uk> on behalf of Makarius <makarius@sketis.net>
Sent: Monday, August 3, 2020 3:18:22 PM
To: Lukas Stevens; cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] Record update syntax

On 03/08/2020 14:38, Lukas Stevens wrote:

The application is exactly src/Provers/order.ML but I'd like to refactor
the interface of the prover to reduce boilerplate on the ML side of
things. Reducing boilerplate when instantiating the prover would also be
great. One way is, as you suggested, to just use tables instead of
records. This would increase the opaqueness of the code since it hides
which theorems are needed exactly.

In that case, I do propose to use a plain table that maps a thm name to thm
value: the Order_Tac module has already several operations that use (untyped)
string "tags" instead of typed record fields, so it fits stylistically and
actually simplifies the current situation (notably operations like "empty" and
"update"; the odd dummy_thm will disappear, it is replaced by an undefined
table entry).

As you proceed to explore order.ML and learn idiomatic use of Isabelle/ML, you
will find more and more ways to make the implementation concise and to the point.

(The file name should be actually order_tac.ML in correspondence to structure
Order_Tac in it.)

There is yet another perspective on the problem: type less_arith is like an
algebraic structure with "laws" for operations (=), (<=), (<). This could in
principle become an axiomatic specification as a locale context, and the tool
then operates "under a morphisms" to move it from the abstract context to
application contexts.

Then the record disappears altogether and is replaced by fancy operations on
logical context elements (due to locale interpretation). An example for this
approach is src/HOL/Tools/semiring_normalizer.ML but it has its own added
complexity.

Another way would be to use the
antiquotations you proposed. Especially the generalised antiquotation
would be great and also make sense since records can be viewed as tuples
with names instead of indices.

Right now I recommend to concentrate on the core problems of the application,
and ignore accidental inconveniences of records in Isabelle/ML.

Makarius


Last updated: Dec 05 2021 at 22:18 UTC