Re: [isabelle] Proof of concept: BNF-based records

Lars discussed this with me. There is no harm in putting it in Library as long as the functionality and limitations of this approach are clearly stated in the theory, which they are currently not. This needs to be included. Then people know what they are letting themselves in for.


On 14/02/2018 15:01, Makarius wrote:
On 08/02/18 22:36, Lars Hupel wrote:

I'd like to demonstrate that it is quite simple to base records on BNFs.

The short story is: it takes about 160 lines of ML code and 50 lines of
syntax declarations to achieve almost (one big caveat, see below)
feature parity to the standard record package (sources attached).

This is all very strange. No discussion whatsoever and now there is even
a change on the Isabelle repository:

The history of the official Isabelle record package is long and
entangled. Initially its main idea was to support extensible records in
a simple manner (see the paper by Naraschewski and Wenzel from 1998).
Later, some guys from Sydney added many more features to make the
package scalable for the L4.verified project -- that made the
implementation also very complex. Thus it has become difficult to update
and "localize" it. Moreover any connection to BNF datatypes (which are
very resource hungry) is likely to bomb applications with many record
fields (or record extensions).

It is presently unclear to me, where the scalability features are used
in practice. If L4.verified no longer requires that, we can probably
remove 80% of the record package and then update it easily. If scalable
records are still required, it will need more work to update.

Can some Data61 people say more about their current applications of the
record package?

Looking for your input on whether this is useful, and whether it belongs
into HOL-Library, the AFP, or the bin.

Spontaneously, I would have said HOL-ex or the bin. By putting it in
HOL-Library, you make certain claims of quality and sustained
maintenance. I.e. the first posting I can imagine on isabelle-users:

"I've found out about HOL-Library.Datatype_Records by accident -- there
is no NEWS entry and no documentation whatsoever. That tool appears to
be in conflict with the existing record package. Can anybody please fix
this ASAP, such that I can use theories with regular records together
with these new BNF records? Anyway, what is the roadmap? Can I expect
new BNF records will eventually supersede old-fashioned typedef records?"

What is supported? Pretty much the old syntax:

   bnf_record ('a, 'b) foo =
     field_1 :: 'a
     field_2 :: 'b

   term "⦇ field_1 = 3, field_2 = () ⦈"
   term "foo ⦇ field_1 := y ⦈"

Also, record construction syntax is supported out of the box for
arbitrary single-free-constructor types:

   datatype x = X (a: int) (b: int)

   term "⦇ a = 1, b = 2 ⦈"

Update syntax for existing types can be installed like this:

   local_setup ‹BNF_Record.mk_update_defs @{type_name x}›

   term "(X 1 2) ⦇ b := 3 ⦈ = X 1 3"

That is record notation with "make" and "update" operations on top of
existing datatypes. It was actually the plan in 1996/1997, before the
extensible record scheme emerged in 1998. We did not do this by fancy,
but it was based on requirements from applications.


The longer reason: there are more problems with records, e.g. there is
no support for nested recursion (they do not constitute BNFs), and even
"copy_bnf" can't fix the absence of a suitable "size" function (which
makes termination proofs impossible).

Can you explain this further? Is there an inherent problem of the
general idea of the regular record package wrt. BNFs? Can the BNF
experts comment on that?

Why not?

The internal construction of standard records is much faster. Half of
the 50 lines to declare syntax is required to un-declare record syntax.
Unfortunately raw "syntax" rules can't be bundle-d. Importing the theory
breaks all existing record syntax.

BTW, there is an old Isabelle development principle to be monotonic wrt.
existing tools. A fork and clone is bad enough, one that disrupts what
is already there is worse: entropy, decay.

What is the motivation for this?

Lem supports records. CakeML uses them for some core types, and
specifies nested recursion through them. Whenever CakeML updates, I can
either change the generated sources to include a bunch of magic
incantations to make termination proofs work, or I can change Lem to
emit "bnf_record" instead of "record".* As a third option (somewhere
between band-aid and proper solution), Jasmin has already suggested a
few months to port the size plugin to records. I attempted that but
unfortunately it took me too much time and ultimately I didn't manage
to. This here was much quicker to pull off (approx. 3 h) and fixes an
immediate problem I had. (Jasmin did however prevent me from writing a
plugin that generates update functions for all datatypes.)

This hints at various discussions in the dark. We have relatively little
traffic on the isabelle-users and isabelle-dev mailing lists, so why not
use them for proper discussions?

As a reminder:

   * isabelle-users is for anything that is relevant to users of official
Isabelle releases (past, present, future releases).

   * isabelle-dev is for anything concerning the ongoing development
process of Isabelle repository versions between releases.

   * It does not make sense to cross-post on both lists; isabelle-dev is
the smaller list, essentially a subset of isabelle-users.

Mailing lists are not for real-time "chats". Often the relevant people
are not immediately reactive (e.g. busy somewhere else or even on
vacation). This means it needs more than just a few days to draw
conclusions from the absence of postings.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.