Skip to content

revise existing tests to match #311 (subtype checking only for refere… #323

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.

Sign up for GitHub

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

Open
crusso wants to merge 12 commits into
base: master
Choose a base branch
from
Open

revise existing tests to match #311 (subtype checking only for refere… #323

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
9b0e92e
revise existing tests to match #311 (subtype checking only for refere…
crusso Mar 18, 2022
6976902
More test cases, new file for subtype tests
nomeata Apr 8, 2022
734b796
Many more tests
nomeata Apr 8, 2022
135a26e
Tests about infinite types
nomeata Apr 8, 2022
5e8c752
Use method name "m" to work around https://github.com/dfinity/motoko/…
nomeata Apr 9, 2022
0889e28
A few tests with future types
nomeata Apr 9, 2022
9420864
Update test/construct.test.did
nomeata Dec 5, 2022
98ea8ed
Update test/subtypes.test.did
nomeata Dec 5, 2022
ad0dc5b
Merge branch 'master' into claudio/candid-subtype-check
nomeata Dec 5, 2022
086e43e
add "(µ record) <: (μ (record opt))"
nomeata Dec 5, 2022
d2b7b81
Merge branch 'master' into claudio/candid-subtype-check
chenyan-dfinity Dec 5, 2022
96718cf
Merge branch 'master' into claudio/candid-subtype-check
crusso May 25, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions test/prim.test.did
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -195,5 +195,6 @@ assert blob "DIDL\00\01\71\03\e2\28\a1" !: (reserved) "reserved from invalid utf
assert blob "DIDL\00\01\6f" !: (empty) "cannot decode empty type";
assert blob "DIDL\01\6e\6f\01\00\00" == "(null)" : (opt empty) "okay to decode non-empty value";


assert blob "DIDL\00\0a\7f\7e\7d\7c\7f\70\7f\7b\7a\79\01\2a\2a\2a\2a\00\2a\00\00\00"
== "(null, true, 42, 42, null, null, null, 42, 42, 42)" : (null, bool, nat, int, null, reserved, null, nat8, nat16, nat32) "multiple arguments";
4 changes: 2 additions & 2 deletions test/subtypes.test.did
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,8 +124,8 @@ assert blob "DIDL\02\6a\00\01\01\00\6b\01\00\7e\01\00\01\01\00\01m"

assert blob "DIDL\02\6a\00\01\01\00\6c\01\00\01\01\00\01\01\00\01m"
== "(opt func \"aaaaa-aa\".m)" : (opt func () -> (EmptyRecord)) "(µ record) <: (µ record)";
//assert blob "DIDL\02\6a\00\01\01\00\6c\01\00\01\01\00\01\01\00\01m"
// == "(null)" : (opt func () -> (empty)) "(µ record) </: empty";
assert blob "DIDL\02\6a\00\01\01\00\6c\01\00\01\01\00\01\01\00\01m"
== "(null)" : (opt func () -> (empty)) "(µ record) </: empty";
Comment on lines +127 to +128
Copy link
Copy Markdown
Contributor

@chenyan-dfinity chenyan-dfinity Dec 4, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
assert blob "DIDL\02\6a\00\01\01\00\6c\01\00\01\01\00\01\01\00\01m"
== "(null)" : (opt func () -> (empty)) "(µ record) </: empty";
// assert blob "DIDL\02\6a\00\01\01\00\6c\01\00\01\01\00\01\01\00\01m"
// == "(null)" : (opt func () -> (empty)) "(µ record) </: empty";

I will comment out this test for now. It's a bit implementation dependent. In Rust, we replace µ record with empty after parsing the type table, so we actually get opt func instead of null.

Copy link
Copy Markdown
Contributor Author

@crusso crusso Dec 4, 2022

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.

Copy link
Copy Markdown
Contributor

@nomeata nomeata Dec 5, 2022

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.

Copy link
Copy Markdown
Contributor Author

@crusso crusso Dec 5, 2022

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.

Copy link
Copy Markdown
Contributor

@nomeata nomeata Dec 5, 2022 •
edited
Loading

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 :-)

assert blob "DIDL\01\6a\00\01\6f\00\01\00\01\01\00\01m"
== "(opt func \"aaaaa-aa\".m)" : (opt func () -> (EmptyRecord)) "empty <: (µ record)";
assert blob "DIDL\02\6a\00\01\01\00\6c\01\00\01\01\00\01\01\00\01m"
Expand Down