RFC: If hypothesis scope

Stream: lean4

[Tom]

Here's a MWE:

def test_single_arm (val : Nat) : Nat := Id.run do
  if h: val != 0 then
    return 0
  -- h not in scope here
  return 1

As far as I can tell, this is due to the fact that in the parser and elaborator, this just gets converted to an if with an empty else branch. I can confirm this by adding the else and voila, not h is in scope in the else.

However, this makes writing code with early returns a bit "clunky", esp if I wish to use h later on. Some examples of the code I am trying to make "easier" are here

It seems the crux of the problem is in doIfToCode in Elab/Do.lean. Baring doing some more advanced flow analysis, I thought perhaps that I could change the logic in this function so that

1) It would check for the empty else case
2) Check if the last statement of the of the if statement is a control flow statement
3) Move the rest of the do statement into the else branch

I built a prototype PR here. Note that this is my first time looking at Elab/Syntax and I pretty much worked it out by reading the code so please, please, I would appreciate any feedback!

Let me know if this is of interest and I can try and convert from "draft" to a full PR. Thanks!

[Mario Carneiro]

changes to Elab/Do.lean have been rejected in the past. The code is frozen

[Eric Wieser]

I think probably this could at least be converted into a full RFC on github

[Tom]

@Mario Carneiro

Thanks for the heads up! Why is the code "frozen"?
Just so I know/don't "waste time", are you aware of other areas of the compiler which have a similar status?

[Tom]

@Eric Wieser

Thanks, I will. However, I've already written another RFC about ranges and didn't want to generate too many... with this PR, I was showing I was also willing to do the work rather than just suggest features.

[Mario Carneiro]

Tom said:

Mario Carneiro

Thanks for the heads up! Why is the code "frozen"?
Just so I know/don't "waste time", are you aware of other areas of the compiler which have a similar status?

Because it doesn't have a designated maintainer. The person who wrote the code (Leo) has a million other things to do and this is a very low priority area. I'm just reporting my experiences trying (and failing) to get features through to set your expectations.

I don't know any other area quite like that, but if you wanted to make changes to the kernel or the new compiler (and probably most nontrivial changes to the old compiler) I doubt you would be successful unless you are on the FRO payroll. Many core parts of the elaborator are also very difficult to get changed, even when there are good reasons to, see example.

[Tom]

Thanks @Mario Carneiro , I appreciate the explanation and will keep it in mind!

I didn't fully expect for the PR to be accepted and hence why I made it just a draft/proof of concept. Based on your feedback, I may just turn it into a full PR and see if gets rejected and if so, I will move on.

What is the "new compiler"? Is this the new "code generator" Henrik B has mentioned before?

[Mario Carneiro]

yes

[Kyle Miller]

Off the top of my head, parts of the code base that are currently "frozen" from accepting external contributions are

• do elaboration
• the compiler
• typeclass instance synthesis
• the defeq algorithm and core algorithms for metavariables
• the kernel

Many of these are pretty much off-limits to the FRO as well at the moment.

I'd say that for external contributors, generally issues > RFCs > PRs. Going from one step to the next takes significantly more work and discussion. We want issues that show concrete problems users are facing, which helps guide how development resources are applied.

The MWE in your first post in this thread is almost good for an issue, but it's a bit artificial and doesn't illustrate the need for the feature on its own. It takes some imagination to come up with applications. It's also sort of low-priority since the workarounds are easy (use a multi-arm if). Please create an issue showing a use case that illustrates early return and needing h!

Let's say we've boosted this to a real issue and we've determined that fixing it has suitable impact (as judged by say the FRO's triage team). To get to the next step of an RFC, we'd want to also analyze control flow in general. My first thought is that unless is also a single-arm if, and if we are touching if wouldn't we want to also make unless accept a hypothesis for completeness?

Then lastly there's getting to creating an implementation. Proofs-of-concept can be helpful for helping evaluate potential changes of course, but when touching core components, the FRO tends not to accept unasked-for external contributions. Leo has some justification for this in the Github comment.

In my opinion, the most important work is identifying and minimizing problems and writing them up as clear issues. I don't believe implementation is the limiting factor in most cases.

It's a lot easier to make contributions to downstream projects like Batteries and Mathlib, and they have a lot more low-hanging fruit for new contributors, with plenty of tactics and plenty of missing theorems.

[Tom]

First of, let me say thank you for such a thorough explanation, this is information which is not easy to find and I saved this message for later reference.

Let me answer some of your comments:

any of these are pretty much off-limits to the FRO as well

Wow, what does that mean? Who maintains/works on these then?

I'd say that for external contributors, generally issues > RFCs > PRs

I will try and adjust my mindset then. My previous experiences with OSS projects have been that "feature requests are cool, but PRs are cooler", and sometimes downright just "if you want this, make a PR".

The MWE in your first post in this thread is almost good for an issue,

I updated the PR description some of the code from the tests. I had linked to the examples above but I understand they should be more front and center.

[Tom]

As for additional examples, I can certainly make them and create an issue. The PR itself is a stepping stone in my current work on trying to make array indexing "nicer".

• I have a PR already merged which tries to "clean up" some usages of []! in the Lean source
• I have submitted an RFC (linked above) regarding iteration with Ranges

Next, I wanted to work on support for indexing multiple arrays (eg. by looking at the into the get_elem_tactic). In the Lean source, there is pattern of iterating multiple arrays and indexing as arr1[i]! because the for hypothesis only supports Membership of the array involved in the Range; however, the code frequently leads with e.g.

if arr1.size != arr2.size:
   return ...

-- Now iterate both arr1 and arr2 but still have to use `[]!`

This is the "real" motivation behind the PR but it seemed wrapping it up in a separate improvement may make sense.

Note while you are correct that one could add an else, the fact that people write code like this suggests is that it's in some sense "easier", which is why I'm trying to learn more by going after some of these "paper cuts".

[Tom]

and if we are touching if wouldn't we want to also make unless accept a hypothesis for completeness?

I have noticed this and reported it here

(Update: I have filed an issue for the unless syntax, as requested: Issue 5598)

[Tom]

the FRO tends not to accept unasked-for external contributions

Understood. The PR is supposed to serve two purposes:
1) Show an example of a working implementation and the problem is solved
2) (and as I mentioned above regarding the other OSS projects) "putting my money where my mouth is", so to speak

It's also a good learning exercise for me working in the code base but that is of no value to people out :smile: side of myself

[Tom]

<deleted/moved above>

[Kyle Miller]

Lean core is developed as a "cathedral" instead of a "bazaar". Think the Linux kernel, where there's an architect in charge, who's delegated authority over certain subsystems. You wouldn't expect Torvalds to want to see a patch to change the process scheduler without a lot of discussion first, right? Even changing the max/min macros has needed his personal approval.

I appreciate your enthusiasm, but with multi-indexing you shouldn't be working on your own. You'll need to work with the FRO here to make an acceptable design and to make sure it is consistent with whatever work may currently be in progress internally. Also, unless you have some project that really depends on it, that can't be done with user libraries, I don't think you can expect this to be an FRO priority. The hard work here is making a clear case for it addressing a user need. There's also potentially evaluating the design space, though that requires being well-acquainted with the language and its design patterns.

[Mario Carneiro]

Tom said:

Many of these are pretty much off-limits to the FRO as well

Wow, what does that mean? Who maintains/works on these then?

No one. That's what "frozen" means. It isn't broken, nobody try to breathe too hard on it in case we cause bigger issues.

[Tom]

Understood and FWIW, I'm good with that!

I am not sure if this is coming across in my messages but I don't have some "grand plan" that I'm trying to push and I am very open to feedback.

I didn't set out to "fix" array indexing, nor to implement the other changes - it is a lot more organic than that. Due to my relative inexperience, my focus is narrow and I "dig" around areas to grow my understanding. The changes I made are a representation of the "early journey feedback", which sometime has value due to the fact that once one gets used to an ecosystem, they don't see/worry about the "beginner paper cuts" anymore.

So, I am trying to learn Lean and adjust my mindset coming from other languages. Arrays and iteration is something most beginners will run into very early on. In my case it was a bit like:

1. I try to use "[]" and wonder why I need "[]!
2. Then, assuming Lean source and its libraries would be a good place to view/learn best practices, I realized that it's a lot more common. Wait, wasn't the language supposed to be safe/provably safe?
3. Hm, what am I misunderstanding...? <dig more>
4. Hm, here's a feature which may be useful in isolation... etc.

So, I am running into some issues and I'm trying to report/file them as RFCs, e.g.

• Range behavior
• Dependent iteration with ForIn
• Some Float behaviors
• etc

However, I am a little worried because I don't want to just point out issues and rather try to be helpful with resolving them.

[Mario Carneiro]

Lean runs a lot more like a company than the average OSS project. I'm sure https://github.com/microsoft/vscode would rather you open an issue rather than try to fix it yourself

[Patrick Massot]

I would rather say that the core of Lean core is a lot more complicated than the average OSS project. So beginners trying to improve things there are a lot less likely to be useful.