Editable typedefs stage 1

[georgefst]

PRIM-12

Note that we use "RHS" ("right-hand side") to refer to the results of match branches, which makes sense with the Haskell-style rendering used in this document, but in Primer, we may not actually render them on the right hand side - we could do with better terminology.

Note also that any annotations appearing in examples need not necessarily be present in programs. They are used here effectively as meta-information, to make types clearer to the reader. Though when explicit annotations do exist in the program, we will have to adapt them as shown.

Description

This is a feature request.

Currently, type definitions ("typedefs") can not be modified after they are first created. This is obviously unsatisfactory. Students should be able to make changes to their type definitions and refactor their programs to match, as is possible in any other language.

Note that currently when we change the type of a variable, we put each existing occurrence of that variable in to a non-empty hole. We will try to handle typedef edits similarly, where it makes sense.

Prior art

Hazel also puts variables in to holes when their types change. Though since Hazel doesn't have user-defined types, it does not have anything else to teach us here.

Unison is seemingly able to deal with changes to type declarations, though unfortunately the docs on that are not written yet (at time of writing, there's just the heading "Refactoring type declarations" and text "🚧 Unfortunately, this section is still UNDER CONSTRUCTION" EDIT: Unison has just had a major update, with new docs, but I still can't find anything about modifying types). Regardless, from how they handle other changes, we can assume that a new type is created, and the old one also kept. Unison is built around making it ergonomic to have a load of copies of everything hanging around. I suspect that we couldn't do what they do and make it usable in Primer without buying in to their whole philosophy, but this may be worth further investigation: see "future work".

Spec

This section categorises the changes we can make to a typedef, and explains how we should handle them. We will only perform these operations when the program does not otherwise typecheck. In the case of an expression already in a hole, or a top-level definition with no type annotation, this may not always be the case.

Rename type, constructor, or type parameter

We need to modify every use site to match the new name, as we do currently when renaming a variable. When renaming a type, we will also need to update its name where it may appear in the constructors of other typedefs.

Note that in the case of type parameters, the name isn't even used in the body of the program. It's only a local binding within the typedef.

Add type

There's really nothing to do.

Add constructor: data T = A -> data T = A | B

We can just add another branch to every match on that type, the RHS being a hole:

Before:
match (t : T) with A -> a

After:
match (t : T) with A -> a ; B -> ?

Change type of a constructor's parameter: data T = A X Y -> data T = A X Y'

We can mostly respond similarly to when the type of a normal variable changes.

Construction

When A is saturated as far as the edited parameter, we can just put the corresponding argument in to a hole.

Before:
A $ x $ y

After:
A $ x $ {? y ?}

If A is only partially saturated, we may have to put the whole application in to a hole, since it remains well-typed, but its type has changed.

Before:
A $ x : Y -> T

After:
{? A $ x : Y' -> T ?}

Deconstruction

Put any occurences of the variable whose type changed on the RHS in to holes, if necessary to make the program typecheck.

Before:
match (t : T) with A x -> f $ x

After:
match (t : T) with A x -> f $ {? x ?}

Add parameter to constructor: data T = A W X Z -> data T = A W X Y Z

Construction

When A is saturated as far as the new parameter, we just add a hole for the argument corresponding to the new parameter.

Before:
A $ w $ x $ z

After:
A $ w $ x $ ? $ z

Otherwise, we'll put the whole expression in a hole, since it remains well-typed, but its type has changed.

Before:
A $ w

After:
{? A $ w ?}

Deconstruction

We can just add another variable binding - the RHS needn't change.

Before:
match (t : T) with A -> a ; B y -> b

After:
match (t : T) with A -> a ; B x y z -> b

Not in spec

Type parameters

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.

Deletion

The deletion of parts of a type definition is harder to handle, since we want to avoid the student losing code that they've written. In addition to the operations outlined above, the following are also possible:

• Delete type
• Delete constructor
• Delete parameter from constructor
• Delete parameter from type
  • Concerns about losing code are somewhat lesser here in practice, but a student could in theory have an arbitrarily-complex type-level expression in a no-longer-required type application.
  • Note that we can only allow this when the parameter does not appear in any constructors. Or at least, we should remove the parameter from any constructors automatically as a first step.

We should consider these alongside other changes which can cause code to disappear. See Saving the student's work when a type changes.

More flexible patterns

See #132 (comment).

Currently, the branches in a case expression are disjoint and automatically generated based on the type of the scrutinee. But we will probably eventually allow more powerful pattern matching. This may complicate the handling of typedef edits.

Catch-all "wildcard" patterns shouldn't change anything much. In the "Add constructor" case there would be fewer changes to the program needed - if a match block contains a wildcard, then that would swallow up any new constructors. But there is also a possibility that deleting parts of a typedef could make a wildcard redundant.

Nested patterns will also need to be considered.

Name hints

When changing the type of a constructor's parameter, should we re-apply name hints? We'd need to keep track of which names come from hints.

The benefits of this are fairly small, and it may even be confusing to a student to see a variable's name change without their input.

Re-ordering

It would be nice to have first-class support for re-ordering parts of a typedef.

We may want to be able to re-order constructors. Currently, order of constructors does not matter semantically, but visual organisation could be important for understanding. Some day, we may also have code generation features which rely on the ordering of constructors (such as Haskell's deriving Ord).

We'll also want to be able to re-order parameters to (type and value) constructors. This could be awkward in the case of partially-applied constructors, one option being to insert lambdas to flip things around as necessary.

Future work

Allow deleting or re-ordering parts of a typedef, and handling changes to type parameters - see "Not in spec".

It may be worth trying out Unison, to see exactly what they do, assuming that, while undocumented, support has been implemented. @dhess has proposed that we could replicate their functionality via our module system somehow, e.g. by creating a new module for each successive version of a type. But I believe the solutions we're proposing in this feature request are straightforward enough that we should go ahead and implement them first regardless.

When we have #321, we will need to propagate changes to dependent modules.

Note that all of the actions described above are very incremental. For example, we can't add a constructor with fields in one step. We could actually remove the existing AddTypeDef, leaving only a basis of minimal actions. This would actually go half way to solving hackworthltd/primer-app#381.

[dhess]

Note: discussed in our 2022-03-01 Primer definition meeting here: https://docs.craft.do/editor/d/8b43f204-aeeb-b8ce-45cc-73a653745299/de670427-bf09-4c58-bab1-75b9dfeaae39

[georgefst]

We can just add another branch to every match on that type

There's an overlooked implementation detail here: how, in general, do we determine the scrutinee's type? It seems that we can't always rely on TypeCache metadata always being present. We can try to syntheseise a type, but this can be expensive, and besides, we process these actions in applyProgAction, which doesn't currently have the right context to call synth.

@brprice any ideas on how best to proceed?

[brprice]

We can just add another branch to every match on that type

There's an overlooked implementation detail here: how, in general, do we determine the scrutinee's type? It seems that we can't always rely on TypeCache metadata always being present. We can try to syntheseise a type, but this can be expensive, and besides, we process these actions in applyProgAction, which doesn't currently have the right context to call synth.

@brprice any ideas on how best to proceed?

Ah, yes, that is a bit awkward. I have two ideas, neither of which I particularly like:

1. ensure we are in a scenario where we can rely on the TypeCache. The reason we cannot rely on it is that it is broken in the middle of a sequence of actions (I cannot remember details here about timing -- possibly only in a BodyAction or SigAction))-- as we may made some changes but not run a typecheck yet to refresh the cache. Thus we could just ask that, for example, the "edit a typedef" action is run standalone. (If we do this, we'd best check that the cache is up to date at the end of any action sequence -- in particular, we'd need to handle the case of renaming a typedef)
2. don't mess with branches, but rely on the TC run that (hopefully?) runs after this action to use smartholes and insert the new branch

However, are you sure that you cannot just synth: that seems to be what we do when we construct a case expression in the first place.

[georgefst]

However, are you sure that you cannot just synth: that seems to be what we do when we construct a case expression in the first place.

Aha, thanks. I see now that we actually create new Cxts all over the place, so this is presumably fine. We can just use:

t <-
  fst
    <$> runReaderT
      (synth _)
      (buildTypingContext _ _ _)

and add a constructor to ProgError which contains a TypeError.

[georgefst]

Something else which wasn't considered above: what to do with metadata? e.g. when we end up with types in metadata with the wrong name.

Should we just take the safe option and traverse all expressions, wiping all TypeCaches? We might be able to recover from simple edits like renaming, but other edits may mean that types in metadata are no longer well-formed anyway.

[brprice]

Something else which wasn't considered above: what to do with metadata? e.g. when we end up with types in metadata with the wrong name.

Should we just take the safe option and traverse all expressions, wiping all TypeCaches? We might be able to recover from simple edits like renaming, but other edits may mean that types in metadata are no longer well-formed anyway.

I think the safe option is to do a full TC pass after the edit, which will re-populate all the caches. This would ensure that (a) the frontend gets up-to-date info and (b) that we will get an error message promptly if there is a bug in the action code which makes the program ill-formed.

[georgefst]

I think the safe option is to do a full TC pass

To be clear, does "a full TC pass" mean calling synth and synthKind on everything?

[brprice]

I think the safe option is to do a full TC pass

To be clear, does "a full TC pass" mean calling synth and synthKind on everything?

The overkill way is to use checkEverything, but depending on what the edit is it may be more efficient to call some smaller-scale TC function on the changed bits.