Better lambda normal form

[neko-kai]

Instead of substituting lambda parameters with fake parameters to generate normal form, we should generate normal forms for lambdas in a format that can also be used as their primary form, e.g. given 2 nested lambdas:

λ %0:0/1 → Applicative3[λ %1:0/3, %1:1/3, %1:2/3 → 0:0/1[1:1, 1:2]]

Current normal forms are:

1. Applicative3[λ %1:0/3, %1:1/3, %1:2/3 → FAKE_0[1:1, 1:2]
2. 0:0/1[FAKE_0, FAKE_1]

Should be:

1. Applicative3[λ %1:0/3, %1:1/3, %1:2/3 → 0:0/1[1:1, 1:2]]
2. -1:0/1[0:1/3, 0:2/3]

Where -1 refers to outer context 1 level up, -2 refers to outer context 2 levels up, etc.

[jdegoes]

/bounty $150

[pshirshov]

There are several ways to address this. If someone wishes to work on this, I would advise to apply normalization in the constructor of LightTypeTagRef.Lambda, that should be a simple recursive rule just renumbering the parameters starting from the innermost structures (current numbering naturally starts from the outermost ones). So, you dig into the lambda, which is a tree-like structure, and once you reach the leaves, you roll your recursion back inverting the LambdaParamName.depth.

Alternatively, one might look at the application points of LambdaParamName and try to refine our current approach to parameter numbering, although I think while it might be more correct to do so, it's not worth it.

[algora-pbc]

💡 @asr2003 submitted a pull request that claims the bounty. You can visit your bounty board to reward.

[rishi-jat]

/attempt #379

[justinleeyang]

/attempt #379

I can take this bounty. I will start with a focused repro + tests, then submit a small PR and follow up with validation notes.

[justinleeyang]

Quick follow-up on #379: I am still actively working on this. Please let me know if you want me to narrow scope to a smaller first PR.

[justinleeyang]

Quick follow-up on #379: I am still actively working on this. Please let me know if you want me to narrow scope to a smaller first PR.

[justinleeyang]

Quick follow-up on #379: I am still actively working on this. Please let me know if you want me to narrow scope to a smaller first PR.