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.
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
revise existing tests to match #311 (subtype checking only for refere… #323
base: master
Are you sure you want to change the base?
revise existing tests to match #311 (subtype checking only for refere… #323
Changes from 6 commits
9b0e92e
6976902
734b796
135a26e
5e8c752
0889e28
9420864
98ea8ed
ad0dc5b
086e43e
d2b7b81
96718cf
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I will comment out this test for now. It's a bit implementation dependent. In Rust, we replace
µ record
withempty
after parsing the type table, so we actually getopt func
instead ofnull
.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you explain why? I don't quite follow.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In the Haskell code I think I too replace
mu record
with empty, but only after subtype checking?I believe Motoko gets this right as spec'ed.
If we want to allow implementations to differ here we should say so explicitly in the spec. But I don't know if that's a good idea.
Could you introduce in the rust code a
MuRecord
type that you can replace it with, which does the job of preventing your code to run into these vicious cycles, while still having the right subtypes relations?Hmm, but
mu record <: mu (record opt)
, so you probably really can't throw away the structure before subtype checking.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Resolved offline.
\mu record
is shorthand for\mu t. record { 0 = t }
which I agree is isomorphic to empty with least fixed points. Do you agree @nomeata or is it actually not safe to identify them in the type table, even if they are isomorphic.My worry is that Motoko will still distinguish the types that Rust is conflating, which might lead to (obscure) trouble elsewhere.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It’s safe, I think, but it is not according to specification. If we go that route, it would be consistent to equate all other empty types as well (
empty
,{empty, empty}
etc.), and it should be part of the spec. And I would guess that @rossberg doesn’t like it :-)