[tracking] Better name generation

[brprice]

This is a tracking/planning issue for better name generation. A proposal is at https://github.com/hackworthltd/vonnegut/discussions/436. It was also discussed in our 2021-04-20 dev meeting : https://www.notion.so/hackworthltd/2021-04-20-Dev-meeting-a1d4f5d6a6034992b7a4b3cfe0f1e964

---

As a zeroth step, we should consider the questions below, and answer those which need early answers.

As a first pass, we will implement simple idris-style name hints, without worrying about automatic renaming (e.g. making it useful for let bindings). This will need to worry about uniqueness and shadowing etc.

A second pass will be making it more widely useful, especially for let bindings. This may be automatic renaming. Potentially we could do something clever with let bindings in particular, but that is not as widely applicable.
Automatic renaming is a bit worrying, as it could maybe be action-at-a-distance, which is unclear to the user. We may want to restrict it to

• variables which currently have an auto-generated name
• ones which are not used yet
• only ones which we didn't originally know the type (what about if the user changes the type?), rather than renaming to "globally optimise" (e.g. if we have λi1 . ... and wrap it in let _ = ... in λi1 . ... we probably shouldn't choose _ = i1 and rename i1 to j2 for instance).

A third step is to do full fancy name generating described recursively by type.

Another step which can be ordered anytime after the first pass is to offer the user a list of automatically generated choices, rather than just choosing the best one. We should also have a manual rename action which will offer said list (as well as offering it when the variable is initially created).

---

Questions include:

• Tighten up the spec
• How do we manage to uniquify linked names nicely. We would like to generate Cons x1 xs1 and not Cons x xs1 or Cons x1 xs.
• How do we do something nice for type variables. We may well want (in the future) to be able to say forall f. Functor f -> ..., and have the name f chosen automatically. Unfortunately this isn't really captured by the type/kind information f : * -> *, but by the fact that f is used as an argument to Functor, so something needs to change. [Two obvious differences: it is much more common to change the "constraints" later, so we need to worry about automatic renaming; it is simple to have multiple constraints and thus(?) ideas for names, how do we pick the "better" one?]
• When do we not have the type info when we need to pick a name (i.e. when is this feature useless / we really need automatic renaming)? [At least for lets, but there we often get the info "soon": user creates a let, then often the next step is to fill in the bound expr, giving us the type by inference]
• For automatic renaming, what should we do if we start with let h = ? in ..., then see let h = 1 in ... and later let h = show 1 in ... where the type of h is ?, Int, String.
• How do we choose good names for our built in types -- we shouldn't just ape what we are used to. Single letter names are not necessarily good, nor is ...s for lists. If we have longer names, then we may want to be smarter when generating names for List (Maybe (Pair Int Bool)) as list_of_maybe_pair_int_bool is a rather long (and useless?) variable name!

[brprice]

The prs hackworthltd/vonnegut#484 and hackworthltd/vonnegut#508 implement "first pass" and "additional step". We

• Generate names based on type, but only the "major connective", i.e. List Bool and List Int are both just List, and both get xs, ys, zs.
• Take care not to shadow anything, or be shadowed by anything
• But we can have the same name as a binder in a sibling branch (λf . ?) (λf . ?)
• These names are generated on the backend, and then displayed to the user on the frontend, along with a textbox for manually specifying a different name

---

We should think hard about what the default hints are. Currently they are just whatever seemed natural to @brprice when implementing it. These are not necessarily good pedagogically!

---

We do not:

• Do nice naming for solely backend-generated names. This can happen in at least one case: smart holes creates some case branches.
• recursively care about the type: at some point it would be nice if List Bool got ps,qs and List Int got is,js,ns,ms
• Be clever with pattern matches in case branches.
  • We would like case xs of Cons <n> <m> -> ... to make and "match" i.e. Cons y ys is good, but Cons x ys is bad
  • We would like case mi of Maybe <n> -> ... to make match mi, i.e. try to set <n> = i
• auto rename: when creating a let, we do not know the type of the binding (as that is synthesised from the body, which does not yet exist). It may be nice to rename as the user specifies the binding. i.e. go let x = ? in ? to let x = 1 in ? which auto renames to let n = 1 in ?. [Getting the spec here is not done. Do we only do it for auto-gen names? How does that interact with getting the user to choose between a few? What happens if we then change the bound term('s type)? What about foo :: Bool -> Nat; foo = λp . ?, and the user changes Bool to Maybe Bool?]

[dhess]

I think we've probably done as well as we're going to for initial user testing and demos. Removing this from the Demo project tracker.

[georgefst]

A fairly exhaustive list of existing naming conventions, potentially useful as inspiration: https://discourse.haskell.org/t/a-dictionary-of-single-letter-variable-names/10522/7.