Shadowing and metadata

[brprice]

[This is currently a question to build consensus. There is nothing technically wrong, but we could probably do a better job at assigning metadata. Later this issue may evolve into (or be replaced by) a feature request.]

Currently we assign a type to every node of a program, saying "this node has type ...". It is not clear quite what the notion of shadowing means here, and if we want to avoid shadowing.

The high-level trade off is that we need to choose between reflecting types as displayed/given in the program and alpha-converting to avoid "shadowing".

Some examples: what type should we claim the hole in the following terms needs to be filled with?

• letrec y : ∀a.Bool = (let a : ... = ... in ?)
• In an environment where f : ∀a.Bool -> Int (either as a top-level function, or a let-binding, or just that f is some term whose type happens to be as stated), let a = 0 in f ?
• (Λa. ?) : ∀b.∀a. Bool

In each of these cases, we have a hole under a binder a, and the naïve thing to report for the type of the hole is ∀a.Bool. However, this may be confusing as (especially in the case where we have a complex type mentioning a (and other type vars) in the place of Bool) this forall binder shadows some other binder for a.

The other option is to ensure we alpha-convert the reported type to avoid this. For instance, we could say the hole has type ∀c.Bool. However, I worry that this may be confusing because the type "should obviously be ∀a.Bool, as written in the text of the program".

The question more-or-less boils down to: "which is more confusing: shadowing or alpha-conversion?" (Note that because this metadata is entirely generated by primer, we can easily alpha-convert if we want to, whereas the same question about the program text is more difficult -- we wouldn't want to automatically rename the user's program)

(NB: whilst some of these examples have the ∀a shadowing some term-variable binder let a, the question of whether type and term variables are in the same namespace and shadow each other is orthogonal to this question. See #359)

[Edit to add examples from #548

• substTy can introduce shadowing (in both directions, though I only exhibit shadowing an outer here, as that is difficult to fix; it could do a renaming that shadows an inner binder, but this is easy to fix), and this infects (i.e. the assertion in the code that the generated names will not enter the user's program is wrong, at least if you consider the metadata)
  • metadata "checked at" etc for the result of ∀ AA. ∀ a . ∀ BB . AA ∋ Λ BB ?
  • metadata shadows a Λ-bound var in result of ? ∋ Λ a2. Λb. (? : ∀a.∀b.b) b

]

[brprice]

(Mostly a note to myself: I currently have some code on brprice/metadata-shadowing that may be useful: it includes a (failing) property test that typechecking does not cause shadowing (even in the metadata))

Our current thinking is that ideally we should α convert -- by the time this is a problem the student will be using (and hopefully comfortable with) polymorphism and then hopefully alpha-equivalence is well-understood. However, it may be useful to have some UI affordance to explain why renaming happens in only some cases.

However, we also suspect that this situation would be pretty rare. Since neither option is clearly pedagogically better than the other, we should just go with the status quo until and unless more information comes to light showing it is a problem.

[brprice]

We discussed this in the meeting today, and realised a few things.

There are 3 approaches we could take with this issue. To enumerate these, first note that there are two places with names that we care about: the "program text" and the "reported type" (here, I'll just consider the reported type of the hole). For example, in (Λa. ?) : ∀a.T, the program text is (Λa. ?) : ∀a.T, and the reported type is T (I'll format these as <program text> --- <reported type>. The "program text" is the student's input, and the "reported type" is primer's output (note that the reported type is ephemeral, but the program text is persistent). Consider the example (Λa. ?) : ∀b.∀a.Bool --- ∀a.Bool: there is no shadowing in the program text, but the reported type binds an a and is notionally under the Λa, which is the kind of shadowing we are concerned with here. The approaches are:

• do nothing. Shadowing is not necessarily a problem and may be the least confusing thing. We perhaps should have some notification about the shadowing (so a frontend can optionally draw a hint or disambiguate somehow)
• alpha convert in the reported text, so we would say (Λa. ?) : ∀b.∀a.Bool --- ∀c.Bool: This avoids shadowing but it may be more confusing "where did c come from, it is not in the program text". Perhaps there should be some notification about why renaming has happened
• alpha convert in the program text. This (for the running example) has two sub options, corresponding to the two binders:
  • (Λa. ?) : ∀b.∀c.Bool --- ∀c.Bool
  • (Λc. ?) : ∀b.∀a.Bool --- ∀c.Bool

The original examples are maybe a bit sparse (and the choice of Bool misleading), so we elaborate here:

• For the first example, it does not matter if the type mentions a:
  • letrec y : ∀a.Bool = (let a : ... = ... in ?) in ... --- ∀a. Bool
  • letrec y : ∀a.Maybe a = (let a : ... = ... in ?) in ... --- ∀a. Maybe a
• For the second example, where f : (∀a.T) -> Int is in scope, where T will be Bool or Maybe a, it also does not matter
  • let a = 0 in f ? --- ∀a.Bool
  • let a = 0 in f ? --- ∀a.Maybe a
• For the third example however, the choice of Bool was critical, since type abstraction engenders a substitution in types:
  • (Λa. ?) : ∀b.∀a. Bool --- ∀a.Bool everything is fine with Bool: we substitute ∀a.Bool [a/b] and get ∀a.Bool (I expect our current implementation may choose a fresh variable here as it does not inspect Bool to see that b does not appear free)
  • (Λa. ?) : ∀b.∀a. Either a b --- ∀c.Either c a we have been forced to do a renaming (as saying the hole has type ∀a. Either a a is incorrect!)

Perhaps this last example shows that it may be more consistent to always alpha-convert, even if we technically don't need to?