This question came up in our 2022-03-01 Primer deifnition meeting: should we support type definitions with holes?
In our prototype implementation of the frontend, there was no way to construct such a thing (never mind whether the implementation supported it) — if you left anything unspecified in a typedef in the typedef UI, you could not press the "Create" button. Also, there was no way to edit the typedef once it was created.
Now that we're starting work on editable typedefs (see #267), it may be useful to allow the implementation to create holes in a typedef; e.g., as the result of an edit of typedef T which is used as a parameter in typedef S.
Besides any implementation needs, this feature might be useful from a pedagogical perspective. We obviously believe that first-class support for holes in expressions is a useful learning affordance, so why not type definitions, as well?
This question came up in our 2022-03-01 Primer deifnition meeting: should we support type definitions with holes?
In our prototype implementation of the frontend, there was no way to construct such a thing (never mind whether the implementation supported it) — if you left anything unspecified in a typedef in the typedef UI, you could not press the "Create" button. Also, there was no way to edit the typedef once it was created.
Now that we're starting work on editable typedefs (see #267), it may be useful to allow the implementation to create holes in a typedef; e.g., as the result of an edit of typedef
Twhich is used as a parameter in typedefS.Besides any implementation needs, this feature might be useful from a pedagogical perspective. We obviously believe that first-class support for holes in expressions is a useful learning affordance, so why not type definitions, as well?