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

Editable typedefs: type parameters #402

Open
georgefst opened this issue Apr 19, 2022 · 2 comments
Open

Editable typedefs: type parameters #402

georgefst opened this issue Apr 19, 2022 · 2 comments
Assignees
Labels
enhancement New feature or request priority: high This issue has high priority

Comments

@georgefst
Copy link
Contributor

georgefst commented Apr 19, 2022

From "not in spec" section of #267:

Another case to handle is a student adding a parameter to a type: data T x = A -> data T x y = A.

Note that any fresh parameter is, of course, initially unused.

We may want an easy way to allow making a type more or less polymorphic. e.g. converting between data IntList = Empty | Cons Int IntList and data List a = Empty | Cons a (List a).

Note also that if we add or remove parameters, we change a type's kind, and will need to update other typedefs which depend on it.

With #401 being closed, I will use this issue to also track deletion of parameters.

@brprice
Copy link
Contributor

brprice commented Aug 15, 2023

@georgefst Could you update us on the current status of this?

IIUC, we support adding (and deleting) a parameter but only when the type is unused?

@georgefst
Copy link
Contributor Author

georgefst commented Sep 12, 2023

Like #401, I forgot to come back to this issue when this was partially implemented in (the somewhat mis-titled) #1063, adding support for these edits in unused types.

For supporting used types, we need to consider how to fix up type-level expressions where the kind of a type has changed. It might be that this kind/type case is not significantly harder than the already-implemented type/term case. We just have not yet attempted to enumerate all the possible interactions in the manner of #267. Note that when we do so, we should consider deletion of parameters (which overlaps with #401).

Also, note that while the opening comment talks only about adding and removing params, we also support editing the kinds of parameters (#1095), and need to consider how to handle these changes for in-use types.

We also need some unit tests. AddTypeParam and DeleteTypeParam do not appear anywhere in the test suite.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request priority: high This issue has high priority
Projects
None yet
Development

No branches or pull requests

3 participants