New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Record updates should be more polymorphic #173

Closed
mn200 opened this Issue Jun 23, 2014 · 9 comments

Comments

Projects
None yet
3 participants
@mn200
Copy link
Member

mn200 commented Jun 23, 2014

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

This comment has been minimized.

Copy link
Member

mn200 commented Jun 23, 2014

Issue #150 may turn out to be relevant.

@mn200 mn200 added this to the Kananaskis-11 milestone Sep 2, 2015

@mn200

This comment has been minimized.

Copy link
Member

mn200 commented Oct 1, 2015

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

mn200 added a commit that referenced this issue Nov 16, 2015

Work on making record fupd fns more polymorphic
This is github issue #173.

Selftest checks for right behaviour.  But an earlier test is failing
because the handling of "big records" hasn't been completely updated.

mn200 added a commit that referenced this issue Nov 17, 2015

Fixes with polymorphic record literals
1. When you write <| fld1 := foo ; fld2 := bar |> there is secretly an
   ARB term hiding in the result.  You don't want that ARB term to be
   unnecessarily polymorphic.

2. TypeBase.mk_record has to adjust for the possibility that fupds can
   have types of the form

      fupd : (α fldty -> β fldty) -> (α,γ) rcd -> (β, γ) rcd

Continuing work on github issue #173

mn200 added a commit that referenced this issue Nov 17, 2015

Fix proof of "bigrec" thms for polymorphic records
These are the theorems that are proved to knit together the view of the
record that the user expects and the underlying reality, which is a
record of records.  These are stated and proved after the various
underlying record types are defined.

Tests in src/datatype/selftest.sml

This is work on github issue #173

mn200 added a commit that referenced this issue Nov 17, 2015

Get EmitML to handle polymorphic records correctly
Tests in src/emit/theory_tests.

Closes github issue #173
@mn200

This comment has been minimized.

Copy link
Member

mn200 commented Nov 17, 2015

Closed by 9ca8abc

@mn200 mn200 closed this Nov 17, 2015

mn200 added a commit that referenced this issue Nov 17, 2015

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented Jan 3, 2016

This may have broken some CakeML proofs, see e.g., CakeML/cakeml@9259641. There are more breakages, but I haven't figured out what exactly went wrong.

@tanyongkiam

This comment has been minimized.

Copy link
Contributor

tanyongkiam commented Jan 3, 2016

It broke this simplification in clos_relation too: CakeML/cakeml@e4f8eae

@mn200

This comment has been minimized.

Copy link
Member

mn200 commented Jan 4, 2016

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

This comment has been minimized.

Copy link
Member

xrchz commented Jan 4, 2016

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

This comment has been minimized.

Copy link
Member

mn200 commented Jan 4, 2016

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

This comment has been minimized.

Copy link
Member

mn200 commented Jan 15, 2016

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment