Skip to content
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

Improve support for universe-polymorphism #8

Open
flupe opened this issue Sep 29, 2022 · 0 comments
Open

Improve support for universe-polymorphism #8

flupe opened this issue Sep 29, 2022 · 0 comments
Assignees
@flupe
Labels
enhancement New feature or request

Comments

@flupe
Copy link
Owner

flupe commented Sep 29, 2022

What we claim in our paper is that it's fine to encode universe-polymorphic datatypes using our descriptions, as long as quantification over levels happen outside of the description.

However, currently the deriveDesc macro doesn't do this automatically, which means you cannot derive descriptions for universe-polymorphic datatypes right now.

Two approaches:

  • Do as we say in the paper, that is, quantify outside of the description.
  • Do as Josh Ko et al (2022) and add levels that are quantified over in the description.
@flupe flupe added the enhancement New feature or request label Sep 29, 2022
@flupe flupe self-assigned this Sep 29, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@flupe flupe

Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@flupe