Should we support type definitions with holes?

[dhess]

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?

[dhess]

I believe that in #1095, we decided not to support type definitions with holes, as they're not needed since we have *; is that correct, or is it more nuanced than that?

[georgefst]

I believe that in #1095, we decided not to support type definitions with holes, as they're not needed since we have *

The discussion there was just about whether kind-level actions should insert holes, or skip straight to filling them with KType. We opted for the latter, but we do support such holes via the "Delete" action - they just aren't necessary.

Anyway, we now allow type-level holes to appear (in the types of constructor fields), as this is pretty crucial to the design of #949: to be able to incrementally edit types, we need holes to deal with incomplete ones.

[dhess]

Right, thanks.