-
Notifications
You must be signed in to change notification settings - Fork 90
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
Make type annotations to not propagate through merging #1271
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Before this change, a record literal was considered a record type whenever it met a bunch of conditions AND was used in a type position. This meant that `{foo : Number, bar : String}` was always considered as a normal record (fields without definition) when used in a term position. This was already subtly wrong, because this means for example that `x | {foo : Number}` and `let C = {foo : Number} in x | C` are operationally not equivalent. Now that we've made a stronger distinction between static types and contracts (types don't propagate through merging), then this behavior is just unsound. As per this commit, a record literal is considered a record type whenever it satisfies the syntactic conditions, be it in a type or a term position. Additionally, we've forbidden "mixed" style records, that is record literals that are not a record type, but with fields that have a type annotation and no definition. Beside being meaningless, they can be deceiving, and are most often an error or a confusion from users. Either the should use a record type, or use `|` everywhere, as in a record contract.
vkleen
approved these changes
Apr 20, 2023
Co-authored-by: Viktor Kleen <viktor.kleen@tweag.io>
1 task
vkleen
added a commit
that referenced
this pull request
Sep 22, 2023
Because of #1228 we syntactically forbid contracts from containing free type variables. This was implemented in #1271 and #1272. As a result, the double contract application in #1194 became dead code. This PR removes the `%dualize%` primop, the `dualize` field in `Label` and the double application logic when constructing recursive environments for records.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Sep 22, 2023
Because of #1228 we syntactically forbid contracts from containing free type variables. This was implemented in #1271 and #1272. As a result, the double contract application in #1194 became dead code. This PR removes the `%dualize%` primop, the `dualize` field in `Label` and the double application logic when constructing recursive environments for records.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
First step toward fixing #1228. Make type annotations behave differently from contract annotations, and in particular, make them not propagate through merging.
Content
This PR makes a distinction between the contracts coming from a type annotation and the one derived from a contract annotation. In particular, the former aren't stored lazily inside the pending contracts of record fields, nor are they propagated through merging anymore. The contract application for a type annotation is generated statically during program transformations once and for all, making such contract checks local.
Conversion from a record type literal
Doing so, we encountered an interesting issue, which was that the following program was accepted:
Here,
{foo : Number}
was parsed (on currentmaster
) as a record literal with one field and without a definition. But because record contract application is mostly merging, the type annotation{foo : Number}
isn't propagated anymore.But if we write
Then it do report a contract violation, because
{foo : Number}
is now considered first as a record type, then converted to a proper contract (not a record contract, but a builtin special function), and applied correctly.It turns out this is a discrepancy already present on master, and
{foo : Number}
qualifies as a record type but is only considered so in a type position. It's just that on master, the difference between the interpretation as a record type and as a record literal is much less noticeable (but still here: for example, record type contracts currently kill metadata, it's a bug, but this is nonetheless an observable distinction between the first and the second example already on master).This PR makes a record literal qualifying as a record type to be always interpreted as such, even in a term position. As an illustration:
We get an opaque function instead of a record. I think it's mostly fine, because it doesn't make much sense to apply record operations such as merging on such an object anyway. It can be considered the same as
Number -> {_ : String}
, that is some opaque value that can only be applied as a contract.The typed field without definition restriction
After the change, something like
{foo : Number, bar | String}
can be misleading. It's not a record type, so we have the same behavior as the initial problematic example, which is that when used as a contract this expression will never enforce thatfoo
is a number (but it will enforce thatbar
is aString
). Because a freestanding type annotation on a field without a definition doesn't make much sense (after the current change, they are useless, and can be removed to exactly the same effect, because they don't apply to any expression), we simply make them illegal at the parsing stage. That is, you must either write a record type, or you can't write a field with a type annotation but no definition.It might also help people not mixing and confusing type and contract annotations, mostly by forcing them to write contract annotations everywhere inside record contracts, outside record type.
TODOs
{foo = 5} | {foo : String}
fails as expected, butlet Foo = {foo : String} in {foo = 5} | Foo
doesn't. The reason is that the latter isn't inside a type annotation, and is thus parsed as a record literal which is applied through merging, making the type annotation inoperative (which is the point of this PR). I think the solution is to make{foo : String}
to become the contract associated to the corresponding record type all the time, not only inside type annotations. Additionally, we should forbid a type annotation to be attached to a field without a definition inside a normal record, because it's useless (that is, forbid{foo : String, bar | Number}
or{foo : String, bar = 2}
because the type annotation is useless and it might lead to surprising result; it can become a warning later on).