Skip to content

revert subtype theory + syntactic sugar for cloning it #691

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

Jump to bottom
Merged
strub merged 1 commit into from
Feb 5, 2025
Merged

revert subtype theory + syntactic sugar for cloning it #691

strub merged 1 commit into from
Feb 5, 2025

Conversation

@strub
Copy link
Member

@strub strub commented Jan 17, 2025 •
edited
Loading

Current Subtype theory forces to have a type sT for the subtype carrier. This PR is to revert this (i.e. the subtype carrier can be substituted by a user type) but add a command to carefully clone it.

@strub
Copy link
Member Author

strub commented Jan 17, 2025

The standard library has yet to be updated

@strub strub self-assigned this Jan 18, 2025
@strub strub requested a review from fdupress January 18, 2025 09:28
@strub strub marked this pull request as ready for review January 18, 2025 09:28
fdupress
fdupress reviewed Jan 20, 2025
View reviewed changes
@strub strub requested a review from fdupress January 20, 2025 13:58
fdupress
fdupress approved these changes Jan 20, 2025
View reviewed changes
Copy link
Member

@fdupress fdupress left a comment

Choose a reason for hiding this comment

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

Looks good. Should we have a wiki page about this? Could be just a pointer to tests/subtype-clone-sugar.ec to start with.

@strub
Copy link
Member Author

strub commented Jan 20, 2025

Looks good. Should we have a wiki page about this? Could be just a pointer to tests/subtype-clone-sugar.ec to start with.

Yes. I'll be adding one before merging.

@oskgo
Copy link
Contributor

oskgo commented Jan 21, 2025

Does this new mechanism fix the unsoundness I found in #275 (comment)?

If yes, does it still allow making subtypes parametric?

@fdupress fdupress mentioned this pull request Jan 21, 2025
Open
@strub
Copy link
Member Author

strub commented Jan 21, 2025

Does this new mechanism fix the unsoundness I found in #275 (comment)?

If yes, does it still allow making subtypes parametric?

Answered in #275. This PR does not prevent you to assume false in your context. (Let's call, especially in public channel, an unsoundness a proof of false in a close environment)

@strub
Revert subtype theory + syntactic sugar for cloning it
5833578 
The previous Subtype theory forces the definition of the type sT for
the subtype carrier, having multiple `sT` types when one has multiple
subtype instances. This commits reverts this (i.e. the subtype carrier
can be substituted by a user type) but add a command to carefully
clone it.
@strub strub enabled auto-merge (rebase) February 5, 2025 21:43
@strub strub merged commit 46099ed into main Feb 5, 2025
15 checks passed
@strub strub deleted the subtype-theory branch February 5, 2025 22:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@fdupress fdupress fdupress approved these changes

Assignees

@strub strub

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@strub @oskgo @fdupress