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.

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

Device providing ability to use recursive types #1898

Closed
byorgey opened this issue Jun 4, 2024 · 0 comments · Fixed by #1906
Closed

Device providing ability to use recursive types #1898

byorgey opened this issue Jun 4, 2024 · 0 comments · Fixed by #1906
Assignees
Labels
C-Moderate Effort Should take a moderate amount of time to address. L-Capability checking Capability checking determines which capabilities are required by a given piece of code. S-Nice to have The bug fix or feature would be nice but doesn't currently have much negative impact. Z-Feature A new feature to be added to the game.

Comments

@byorgey
Copy link
Member

byorgey commented Jun 4, 2024

#1894 adds a CRectype capability, but it is not used anywhere in the code, and currently it is always possible to use recursive types. Since we went with equirecursive types, there is no special term-level syntax required to use recursive types, and we currently do not do requirements analysis on types.

We should create a device that provides the ability to use recursive types (and restrict their use otherwise). This will necessitate adding requirements analysis for types (which is probably a good idea anyway, e.g. it should not be possible to mention a sum type unless you have an ADT calculator equipped).

@byorgey byorgey added Z-Feature A new feature to be added to the game. C-Moderate Effort Should take a moderate amount of time to address. S-Nice to have The bug fix or feature would be nice but doesn't currently have much negative impact. L-Capability checking Capability checking determines which capabilities are required by a given piece of code. labels Jun 4, 2024
@byorgey byorgey self-assigned this Jun 4, 2024
@mergify mergify bot closed this as completed in #1906 Jun 6, 2024
mergify bot pushed a commit that referenced this issue Jun 6, 2024
Closes #1898.  Adds the `hyperloop` device (recipe: `ADT calculator` + `strange loop`) which provides the ability to use recursive types (#1894).  Also refactors requirements analysis code and adds the ability for types to trigger capability requirements.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
C-Moderate Effort Should take a moderate amount of time to address. L-Capability checking Capability checking determines which capabilities are required by a given piece of code. S-Nice to have The bug fix or feature would be nice but doesn't currently have much negative impact. Z-Feature A new feature to be added to the game.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant