search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

Record updates should be more polymorphic #173

Closed mn200 closed 9 years ago

mn200 commented 10 years ago

If a record has field fld : α, making the type of the record α record, the corresponding update function will have type

record_fld_fupd : (α -> α) -> α record -> α record

There doesn’t seem any good reason to not let it be

record_fld_fupd : (α -> β) -> α record -> β record
mn200 commented 10 years ago

Issue #150 may turn out to be relevant.

mn200 commented 9 years ago

This is only possible if type variables are disjoint across the various fields.

mn200 commented 9 years ago

Closed by 9ca8abc

xrchz commented 8 years ago

This may have broken some CakeML proofs, see e.g., https://github.com/CakeML/cakeml/commit/92596415fd5f2289f4a305342380824a8541e681. There are more breakages, but I haven't figured out what exactly went wrong.

tanyongkiam commented 8 years ago

It broke this simplification in clos_relation too: https://github.com/CakeML/cakeml/commit/e4f8eae7b99d3fa851676858bd7a0ac5f4ffba5e

mn200 commented 8 years ago

Do you think it would be worth adding another piece of syntax that does the update without allowing the polymorphic type to change? (If so, please create an issue for it.)

xrchz commented 8 years ago

If anything the new behaviour should have the new syntax (and the old behaviour the old). However, I'm not sure whether we want the broken CakeML proofs to work as they used to, or whether the extra work we need to put in to make them go through is reasonable. @mn200 do you have an opinion on that?

mn200 commented 8 years ago

I agree that the principle of least backwards incompatibility would call for new behaviour being realised through new syntax. However, in this case I'm fairly convinced that the new behaviour is what we should have had from the outset. I’ve also just realised that it should be possible to get the old behaviour back by overloading the update syntax to a more type-specialised form. Given this I'm even less interested in going back on this.

If you don't figure it out for yourself I hope to be able to show you how to do it later today.

mn200 commented 8 years ago

See commit 34e79290e1 for an example of doing this in the selftest.sml file.