Make TDNR more predictable

[pchiusano]

I'd like TDNR to be more predictable. Lately I've been avoiding it since it gives odd results unless the rest of the code also typechecks (often not the case).

Something that might be relevant is that the way we currently select possibilities is by putting a blank in the program and then running typechecking to learn the type of that blank. If the program has type errors elsewhere, it's possible that inserting that blank may cause the program to typecheck, but with a weird type for the blank.

I'd probably start by collecting a number of examples of behavior we don't like for TDNR, then see if we can come up with something that's highly predictable.

Or it might be that TDNR is fine and just needs better docs and a few bugfixes.

Related issues:

377 #376 #370 #366 #845

[pchiusano]

Some options on the table:

1. rethink it, come up with a more predictable algorithm
2. disable it entirely
3. leave as is, with disclaimers

[francisdb]

https://acronyms.thefreedictionary.com/TDNR ?

[aryairani]

@francisdb IMO, The Dark Night Rises is predictable enough; the one we want to improve is Type-Directed Name Resolution.

[pchiusano]

Current algorithm for TDNR:

1. For each TDNR slot, replace it with a blank, which is a fresh existential, then run typechecking and learn the type of that blank. Based on that type, substitute in the unique matching term, if that exists, otherwise it's a type error.
2. Repeat for the next TDNR slot, until all TDNR slots have been filled. Note that we do N typechecking passes, one for each TNDR slot.

In a program with type errors elsewhere and multiple TNDR slots, sticking a blank with a fresh existential type for each slot is way underconstrained and generates unpredictable results. The blanks can cover up the type errors and cause them to resurface elsewhere (or prevent TDNR elsewhere), and when multiple TNDR slots interact (think foo (x + y), it's also unpredictable).

Alternate algorithm

Here's a single pass algorithm that I think would be predictable:

1. To synthesize a function application, f x y z, where f is a TDNR slot, we first synthesize x, y, and z. Then we see if any of the possibilities for f can be applied to these types. If yes, and it's unique, do it. If no, type error.
2. To check a TDNR slot, f, against a type, t, we do the same - see if any of the possibilities for f are a subtype of t and if it's got a unique solution, use it.

Notice both rules are totally local and can be done in a single typechecking pass. So long as the argument types are known at the point of the call, that type information will be used to select among the functions f. A typical usage is like:

foo : Nat -> Nat -> Nat
foo x y =
  x + y

Here, the synthesized types of x and y (based on the type signature) will be Nat, so the right + is selected. Another possibility is like x + 1, even when x is of an unknown type, since the 1 literal has type Nat and that narrows it down to Nat.+.

Other examples:

• When you have f (g x), as long as the x is of known type, that info propagates and is used to select among g and then f possibilities.
• x |> f also works I think, it will synthesize the type of (|>) x, and if x : Nat is known, that refines the function type to say Nat -> ⅇ, and then checks f against Nat -> ⅇ. If f is a TDNR slot, Rule 2 above then kicks in to refine it.

Some drawbacks:

• fromSequence [1,2,3] doesn't work as a short for Set.fromSequence if there's also like Stream.fromSequence. The arguments to the function aren't refining its type.
• A more TDNR friendly thing would be Sequence.toSet, which you could use as toSet (even if there was also Stream.toSet) as long as the argument to toSet was known to be a Sequence.

It reminds me a little bit of multimethods - dispatch is done based on the types of the arguments. Though the Rule 2 makes it a bit more flexible.

[pchiusano]

Ideas on implementation:

• Give TDNR slots up front access to all their possibilities. I'd just add this information to the blank term / existential type that we already have.
  • Not sure if this matters, but as a simplification, we could only give TDNR access to top-level bindings that have user-provided type annotations. This avoids needing to do multiple passes, one to learn the types of all top-level bindings (but then how do you do that if those bindings use TDNR??). Using TDNR with things that are inferred is likely to just generate confusing errors IMO, when the thing you've inferred has a different type than you expected.
• Get rid of the TDNR monad and just bake Rule 1 and Rule 2 into the typechecking - the blanks will have all the info we need. This will probably be a lot simpler.
• We still have to emit the TDNR decisions so they can be applied to the original term. That could be done right at the point that Rules 1 and 2 are applied (which will be inside of check and synthesize).